--- a/IntEx.thy	Wed Oct 28 01:48:45 2009 +0100
+++ b/IntEx.thy	Wed Oct 28 01:49:31 2009 +0100
@@ -3,7 +3,7 @@
 begin
 
 fun
-  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 
+  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
 where
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
@@ -123,7 +123,7 @@
 lemma intrel_refl: "intrel a a"
   sorry
 
-lemma ho_plus_rsp : 
+lemma ho_plus_rsp:
   "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus"
   by (simp)
 
@@ -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 *}