diff -r 793c3ff4bc2a -r 820c64273ce0 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 08 16:56:51 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 17:35:04 2009 +0100
@@ -307,7 +307,10 @@
 by (tactic {* lift_tac @{context} @{thm m2} 1 *})
 
 lemma "INSERT a (INSERT a x) = INSERT a x"
-apply (tactic {* lift_tac @{context} @{thm list_eq.intros(4)} 1 *})
+apply (tactic {* procedure_tac @{context} @{thm list_eq.intros(4)} 1 *})
+apply (regularize)
+apply (injection)
+apply (cleaning)
 done
 
 lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"
@@ -340,9 +343,8 @@
 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-defer
+apply(injection)
 apply(tactic {* clean_tac @{context} 1 *})
-apply(tactic {* inj_repabs_tac @{context} 1*})+
 done
 
 lemma list_induct_part:
@@ -432,13 +434,13 @@
 sorry
 
 lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"
-apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
+apply(lifting_setup rule: ttt2)
+apply(regularize)
 apply(rule impI)
 apply(simp)
 apply(rule allI)
 apply(rule list_eq_refl)
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
+apply(injection)
 apply(tactic {* clean_tac @{context} 1 *})
 apply(tactic {* clean_tac @{context} 1 *}) (* TODO: needs lambda_prs twice *)
 done