--- a/Quot/quotient_tacs.ML	Fri Jan 15 17:09:36 2010 +0100
+++ b/Quot/quotient_tacs.ML	Sat Jan 16 02:09:38 2010 +0100
@@ -5,7 +5,7 @@
   val all_injection_tac: Proof.context -> int -> tactic
   val clean_tac: Proof.context -> int -> tactic
   val procedure_tac: Proof.context -> thm -> int -> tactic
-  val lift_tac: Proof.context -> thm -> int -> tactic
+  val lift_tac: Proof.context -> thm list -> int -> tactic
   val quotient_tac: Proof.context -> int -> tactic
   val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
 end;
@@ -612,18 +612,24 @@
 
 (* Automatic Proofs *)
 
-val msg1 = "Regularize proof failed."
-val msg2 = cat_lines ["Injection proof failed.", 
+val msg1 = "The regularize proof failed."
+val msg2 = cat_lines ["The injection proof failed.", 
                       "This is probably due to missing respects lemmas.",
                       "Try invoking the injection method manually to see", 
                       "which lemmas are missing."]
-val msg3 = "Cleaning proof failed."
+val msg3 = "The cleaning proof failed."
 
-fun lift_tac ctxt rthm =
-  procedure_tac ctxt rthm
-  THEN' RANGE_WARN 
-     [(regularize_tac ctxt, msg1),
-      (all_injection_tac ctxt, msg2),
-      (clean_tac ctxt, msg3)]
+fun lift_tac ctxt rthms =
+let
+  fun mk_tac rthm = 
+    procedure_tac ctxt rthm
+    THEN' RANGE_WARN 
+      [(regularize_tac ctxt, msg1),
+       (all_injection_tac ctxt, msg2),
+       (clean_tac ctxt, msg3)]
+in
+  simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)  
+  THEN' RANGE (map mk_tac rthms)
+end
 
 end; (* structure *)