--- a/IntEx.thy	Wed Oct 28 16:11:28 2009 +0100
+++ b/IntEx.thy	Wed Oct 28 16:16:38 2009 +0100
@@ -110,12 +110,6 @@
   apply(auto)
   done
 
-lemma equiv_intrel: "EQUIV intrel"
-  sorry
-
-lemma intrel_refl: "intrel a a"
-  sorry
-
 lemma ho_plus_rsp:
   "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus"
   by (simp)
@@ -124,8 +118,8 @@
 ML {* val rty = @{typ "nat \<times> nat"} *}
 ML {* val qty = @{typ "my_int"} *}
 ML {* val rel = @{term "intrel"} *}
-ML {* val rel_eqv = @{thm equiv_intrel} *}
-ML {* val rel_refl = @{thm intrel_refl} *}
+ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *}
+ML {* val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] *}
 ML {* val quot = @{thm QUOTIENT_my_int} *}
 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
 ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *}
@@ -144,34 +138,31 @@
   apply (cases i)
   apply (cases j)
   apply (cases k)
-  apply (simp add: intrel_refl)
+  apply (simp)
   done
 
- ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
+ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *}
+
+
+
+
+
 
 
-text {* Below is the construction site code used if things do now work *}
+
+text {* Below is the construction site code used if things do not work *}
+
+
+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 {* val t_defs_sym = add_lower_defs @{context} t_defs *}
+
 
 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *}
 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
-
-ML {* val t_t =
-  Toplevel.program (fn () =>
-  repabs @{context} t_r consts rty qty
-   quot rel_refl trans2
-   rsp_thms
-  )
-*}
-
-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 {* t_t *}
+ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *}
-
 ML {* val t_a = simp_allex_prs @{context} quot t_l *}
-
-ML {* val t_defs_sym = add_lower_defs @{context} t_defs *}
 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_a *}
 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 ML {* ObjectLogic.rulify t_r *}