--- a/Quot/Examples/FSet.thy	Thu Dec 10 10:36:05 2009 +0100
+++ b/Quot/Examples/FSet.thy	Thu Dec 10 10:54:45 2009 +0100
@@ -343,13 +343,14 @@
 apply(rule list_eq_refl)
 done
 
-lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
+lemma ttt3: "(\<lambda>x. ((op @) x (e # []))) = (op #) e"
 sorry
 
-
-lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))"
-(* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
-sorry
+lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = INSERT e"
+apply(lifting ttt3)
+apply(regularize)
+apply(auto simp add: cons_rsp)
+done
 
 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
 sorry

--- a/Quot/QuotMain.thy	Thu Dec 10 10:36:05 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 10:54:45 2009 +0100
@@ -345,7 +345,9 @@
        else raise (LIFT_MATCH "regularize (bounds mismatch)")
 
   | (rt, qt) =>
-       raise (LIFT_MATCH "regularize failed (default)")
+       let val (rts, qts) = (Syntax.string_of_term lthy rt, Syntax.string_of_term lthy qt) in
+       raise (LIFT_MATCH ("regularize failed (default: " ^ rts ^ "," ^ qts ^ ")"))
+       end
 *}
 
 section {* Regularize Tactic *}