# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259061904 -3600
# Node ID ea27275eba9ae33b93e57a465a296c2bd26f1b5d
# Parent  51aafebf4d06cc1c4d1e9d5a6fce927c05400896
Separate regularize_tac

diff -r 51aafebf4d06 -r ea27275eba9a QuotMain.thy
--- a/QuotMain.thy	Tue Nov 24 08:36:28 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 12:25:04 2009 +0100
@@ -1446,26 +1446,29 @@
 
 (* Final wrappers *)
 
+ML {*
+fun regularize_tac ctxt rel_eqv rel_refl =
+  (ObjectLogic.full_atomize_tac) THEN'
+  REPEAT_ALL_NEW (FIRST' [
+    rtac rel_refl,
+    atac,
+    rtac @{thm universal_twice},
+    (rtac @{thm impI} THEN' atac),
+    rtac @{thm implication_twice},
+    EqSubst.eqsubst_tac ctxt [0]
+      [(@{thm equiv_res_forall} OF [rel_eqv]),
+       (@{thm equiv_res_exists} OF [rel_eqv])],
+    (* For a = b \<longrightarrow> a \<approx> b *)
+    (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
+    (rtac @{thm RIGHT_RES_FORALL_REGULAR})
+  ]);
+*}
 
 ML {*
 fun regularize_goal lthy thm rel_eqv rel_refl qtrm =
   let
     val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm;
-    fun tac ctxt =
-      (ObjectLogic.full_atomize_tac) THEN'
-      REPEAT_ALL_NEW (FIRST' [
-        rtac rel_refl,
-        atac,
-        rtac @{thm universal_twice},
-        (rtac @{thm impI} THEN' atac),
-        rtac @{thm implication_twice},
-        EqSubst.eqsubst_tac ctxt [0]
-          [(@{thm equiv_res_forall} OF [rel_eqv]),
-           (@{thm equiv_res_exists} OF [rel_eqv])],
-        (* For a = b \<longrightarrow> a \<approx> b *)
-        (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
-        (rtac @{thm RIGHT_RES_FORALL_REGULAR})
-      ]);
+    fun tac lthy = regularize_tac lthy rel_eqv rel_refl;
     val cthm = Goal.prove lthy [] [] reg_trm
       (fn {context, ...} => tac context 1);
   in