diff -r 7e6cdcd113a2 -r ee5f79b210c1 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Sep 27 16:44:50 2002 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 30 15:44:21 2002 +0200
@@ -691,7 +691,7 @@
 
 lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
   apply (insert mult_less_not_refl)
-  apply blast
+  apply fast
   done