diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Oct 22 11:01:30 2001 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Oct 22 11:54:22 2001 +0200
@@ -274,18 +274,8 @@
   apply (simp (no_asm) add: expand_fun_eq)
   apply (rule conjI)
    apply force
-  apply clarify
-  apply (rule conjI)
-   apply blast
-  apply clarify
-  apply (rule iffI)
-   apply (rule conjI)
-    apply clarify
-    apply (rule conjI)
-     apply (simp add: eq_sym_conv)   (* FIXME blast fails !? *)
-    apply fast
-   apply simp
-  apply force
+  apply safe
+  apply (simp_all add: eq_sym_conv)
   done
 
 (*