--- a/Quot/Examples/FSet.thy	Tue Dec 08 17:40:58 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 08 17:43:32 2009 +0100
@@ -340,9 +340,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: