diff -r 4fcbbb5b3b58 -r f78aa16daae5 FSet.thy
--- a/FSet.thy	Wed Nov 25 14:25:29 2009 +0100
+++ b/FSet.thy	Wed Nov 25 15:20:10 2009 +0100
@@ -334,6 +334,8 @@
 done
 
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
+apply(tactic {* Induct.fix_tac @{context} 0 [("x", @{typ "'b fset"}), ("xa", @{typ "'b fset"})] 1 *})
+apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 done