--- a/IntEx.thy	Wed Oct 28 15:25:36 2009 +0100
+++ b/IntEx.thy	Wed Oct 28 16:05:59 2009 +0100
@@ -156,7 +156,7 @@
 
 text {* Below is the construction site code used if things do now work *}
 
-ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *}
+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 =
@@ -170,19 +170,13 @@
 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 {*
-  fun simp_lam_prs lthy thm =
-    simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
-    handle _ => thm
-*}
 ML {* t_t *}
-ML {* val t_l = simp_lam_prs @{context} t_t *}
+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 = MetaSimplifier.rewrite_rule t_defs_sym t_a *}
+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 *}