# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256742688 -3600
# Node ID 9d7d9236d9f92e27d38a8c522562bb70e3b86780
# Parent  37b29231265b99c51d7905f9aec8b412b50e3b9b
Fix also in the general procedure.

diff -r 37b29231265b -r 9d7d9236d9f9 QuotMain.thy
--- 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