--- 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