--- a/IntEx.thy	Tue Oct 27 17:08:47 2009 +0100
+++ b/IntEx.thy	Tue Oct 27 18:02:35 2009 +0100
@@ -168,22 +168,16 @@
 ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *}
 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
 
-ML {* val (g, thm, othm) =
+ML {* val t_t =
   Toplevel.program (fn () =>
-  repabs_eq @{context} t_r consts rty qty
+  repabs @{context} t_r consts rty qty
    quot rel_refl trans2
    rsp_thms
   )
 *}
-ML {*
-  val t_t2 =
-  Toplevel.program (fn () =>
-    repabs_eq2 @{context} (g, thm, othm)
-  )
-*}
-
 
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
+
 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
 
 ML {*
@@ -191,8 +185,8 @@
     simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
     handle _ => thm
 *}
-ML {* t_t2 *}
-ML {* val t_l = simp_lam_prs @{context} t_t2 *}
+ML {* t_t *}
+ML {* val t_l = simp_lam_prs @{context} t_t *}
 
 ML {* val t_a = simp_allex_prs @{context} quot t_l *}