--- a/QuotMain.thy	Mon Nov 02 11:51:50 2009 +0100
+++ b/QuotMain.thy	Mon Nov 02 14:57:56 2009 +0100
@@ -760,9 +760,9 @@
 ML {*
 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
   (FIRST' [
-    rtac @{thm FUN_QUOTIENT},
+(*    rtac @{thm FUN_QUOTIENT},
     rtac quot_thm,
-    rtac @{thm IDENTITY_QUOTIENT},
+    rtac @{thm IDENTITY_QUOTIENT},*)
     rtac trans_thm,
     LAMBDA_RES_TAC ctxt,
     res_forall_rsp_tac ctxt,
@@ -873,23 +873,22 @@
     val tac =
       (compose_tac (false, lpi, 2)) THEN_ALL_NEW
       (quotient_tac quot_thm);
-    val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1);
+    val gc = Drule.strip_imp_concl (cprop_of lpi);
+    val t = Goal.prove_internal [] gc (fn _ => tac 1)
   in
     MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
   end
 *}
 
 ML {*
-  fun simp_allex_prs lthy quot thm =
+  fun simp_allex_prs quot thms thm =
     let
-      val rwf = @{thm FORALL_PRS} OF [quot];
-      val rwfs = @{thm "HOL.sym"} OF [rwf];
-      val rwe = @{thm EXISTS_PRS} OF [quot];
-      val rwes = @{thm "HOL.sym"} OF [rwe]
+      val ts = [@{thm FORALL_PRS} OF [quot], @{thm EXISTS_PRS} OF [quot]] @ thms
+      val sym_ts = map (fn x => @{thm "HOL.sym"} OF [x]) ts;
+      val eq_ts = map (fn x => @{thm "eq_reflection"} OF [x]) sym_ts
     in
-      (simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm))
+      MetaSimplifier.rewrite_rule eq_ts thm
     end
-    handle _ => thm
 *}
 
 ML {*
@@ -940,10 +939,12 @@
   val aps = findaps rty (prop_of t_a);
   val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps;
   val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
-  val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_t;
-  val t_a = simp_allex_prs lthy quot t_l;
+  val t_a = simp_allex_prs quot [] t_t;
+  val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
   val defs_sym = add_lower_defs lthy defs;
-  val t_d = repeat_eqsubst_thm lthy defs_sym t_a;
+  val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
+  val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l;
+  val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
 in
   ObjectLogic.rulify t_r