1.1 --- a/src/HOL/Library/Multiset.thy	Fri Sep 27 16:44:50 2002 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Sep 30 15:44:21 2002 +0200
     1.3 @@ -691,7 +691,7 @@
     1.4  
     1.5  lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
     1.6    apply (insert mult_less_not_refl)
     1.7 -  apply blast
     1.8 +  apply fast
     1.9    done
    1.10  
    1.11