--- a/src/HOL/Library/Multiset.thy Fri May 21 17:16:16 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Sat May 22 10:12:49 2010 +0200
@@ -826,7 +826,8 @@
This lemma shows which properties suffice to show that a function
@{text "f"} with @{text "f xs = ys"} behaves like sort.
*}
-lemma properties_for_sort:
+
+lemma (in linorder) properties_for_sort:
"multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys"
proof (induct xs arbitrary: ys)
case Nil then show ?case by simp