# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259072133 -3600
# Node ID 82cfedb16a99a1869b83a63e5ad05d70062af908
# Parent  7a3d86050e72d0110bdabfb9a99200b5873d53ca# Parent  e9bcbdeb3a1ed185190110706f40d5f33766f194
merged

diff -r 7a3d86050e72 -r 82cfedb16a99 QuotMain.thy
--- a/QuotMain.thy	Tue Nov 24 15:15:10 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 15:15:33 2009 +0100
@@ -1600,17 +1600,30 @@
 *}
 
 ML {*
+  fun TRY' tac = fn i => TRY (tac i)
+*}
+
+ML {*
 fun clean_tac lthy quot defs reps_same =
   let
     val lower = flat (map (add_lower_defs lthy) defs)
   in
-    (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN'
-    (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN'
-    (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN'
-    (simp_tac (HOL_ss addsimps [reps_same]))
+    TRY' (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN'
+    TRY' (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN'
+    TRY' (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN'
+    simp_tac (HOL_ss addsimps [reps_same])
   end
 *}
 
+ML {*
+fun lift_tac lthy thm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs =
+  (procedure_tac thm lthy) THEN'
+  (regularize_tac lthy rel_eqv rel_refl) THEN'
+  (REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms)) THEN'
+  (clean_tac lthy quot defs reps_same)
+*}
+
+
 
 end