--- 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