diff -r b00a9b58264d -r bed81795848c FSet.thy
--- a/FSet.thy	Fri Dec 04 09:33:32 2009 +0100
+++ b/FSet.thy	Fri Dec 04 10:12:17 2009 +0100
@@ -299,7 +299,7 @@
 lemma "IN x EMPTY = False"
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply(tactic {* all_inj_repabs_tac' @{context} [rel_refl] [trans2] 1 *})
 apply(tactic {* clean_tac @{context} 1*})
 done
 
@@ -327,7 +327,7 @@
 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 done
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac' lthy [rel_refl] [trans2] *}
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
@@ -389,6 +389,9 @@
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 done
 
 lemma list_induct_part: