--- a/src/HOL/Library/Multiset_Order.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Mon Jul 06 22:57:34 2015 +0200
@@ -62,7 +62,7 @@
have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
unfolding mult_def by (blast intro: trancl_trans)
show "class.order ?le ?less"
- by default (auto simp add: le_multiset_def irrefl dest: trans)
+ by standard (auto simp add: le_multiset_def irrefl dest: trans)
qed
text \<open>The Dershowitz--Manna ordering:\<close>