--- a/QuotMain.thy	Wed Oct 28 16:06:19 2009 +0100
+++ b/QuotMain.thy	Wed Oct 28 16:11:28 2009 +0100
@@ -932,13 +932,10 @@
   val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
   val abs = findabs rty (prop_of t_a);
   val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs;
-  fun simp_lam_prs lthy thm =
-    simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
-    handle _ => thm
-  val t_l = simp_lam_prs lthy t_t;
+  val t_l = repeat_eqsubst_thm lthy simp_lam_prs_thms t_t;
   val t_a = simp_allex_prs lthy quot t_l;
   val t_defs_sym = add_lower_defs lthy t_defs;
-  val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a;
+  val t_d = repeat_eqsubst_thm lthy t_defs_sym t_a;
   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
 in
   ObjectLogic.rulify t_r