--- a/FSet.thy	Fri Dec 04 12:21:15 2009 +0100
+++ b/FSet.thy	Fri Dec 04 14:11:03 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 *})