--- a/QuotMain.thy	Fri Oct 30 16:37:09 2009 +0100
+++ b/QuotMain.thy	Fri Oct 30 18:31:06 2009 +0100
@@ -501,6 +501,10 @@
          else
            Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
        end
+  | Const (@{const_name "op ="}, ty) $ t =>
+      if needs_lift rty (fastype_of t) then
+        (tyRel (fastype_of t) rty rel lthy) $ t
+      else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
   | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
   | _ => trm
 *}
@@ -513,16 +517,25 @@
        (my_reg lthy rel rty (prop_of thm)))
 *}
 
+lemma eq_rr: "(\<And>x. R x x) \<Longrightarrow> a = b \<Longrightarrow> R a b"
+by (auto)
+
 ML {*
-fun regularize thm rty rel rel_eqv lthy =
+fun regularize thm rty rel rel_eqv rel_refl lthy =
   let
     val g = build_regularize_goal thm rty rel lthy;
     fun tac ctxt =
-       (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
+     REPEAT_ALL_NEW (FIRST' [
+      rtac rel_refl,
+      atac,
+      (rtac @{thm  allI} THEN' dtac @{thm spec}),
+      (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
         [(@{thm equiv_res_forall} OF [rel_eqv]),
-         (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
-         (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
-         (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt []));
+         (@{thm equiv_res_exists} OF [rel_eqv])]) i)),
+      MetisTools.metis_tac ctxt [],
+      rtac (@{thm eq_rr} OF [rel_refl]),
+      ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]))
+    ]);
     val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
   in
     cthm OF [thm]
@@ -907,7 +920,7 @@
   val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name;
   val consts = lookup_quot_consts defs;
   val t_a = atomize_thm t;
-  val t_r = regularize t_a rty rel rel_eqv lthy;
+  val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
   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;