diff -r c81f016883df -r a91bab12b2bd src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Nov 07 14:02:08 2006 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Nov 07 14:02:10 2006 +0100
@@ -259,11 +259,11 @@
 
 lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
   by (simp add: multiset_eq_conv_count_eq multiset_inter_count
-    min_max.below_inf.inf_commute)
+    min_max.inf_commute)
 
 lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
   by (simp add: multiset_eq_conv_count_eq multiset_inter_count
-    min_max.below_inf.inf_assoc)
+    min_max.inf_assoc)
 
 lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
   by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def)