--- a/QuotMain.thy	Fri Oct 30 18:31:06 2009 +0100
+++ b/QuotMain.thy	Fri Oct 30 19:03:53 2009 +0100
@@ -517,25 +517,31 @@
        (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)
+lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
+apply (auto)
+done
+
+lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
+apply (auto)
+done
 
 ML {*
 fun regularize thm rty rel rel_eqv rel_refl lthy =
   let
     val g = build_regularize_goal thm rty rel lthy;
     fun tac ctxt =
+      (ObjectLogic.full_atomize_tac) THEN'
      REPEAT_ALL_NEW (FIRST' [
       rtac rel_refl,
       atac,
-      (rtac @{thm  allI} THEN' dtac @{thm spec}),
+      rtac @{thm universal_twice},
+      rtac @{thm implication_twice},
       (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])]) i)),
-      MetisTools.metis_tac ctxt [],
-      rtac (@{thm eq_rr} OF [rel_refl]),
-      ((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]))
-    ]);
+      (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
+      (rtac @{thm RIGHT_RES_FORALL_REGULAR})
+     ]);
     val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1);
   in
     cthm OF [thm]