diff -r 7c6a970f0808 -r de0f4a63baa5 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -47,9 +47,9 @@
   set_of :: "'a multiset => 'a set"
   "set_of M == {x. x :# M}"
 
-instance multiset :: ("term") plus ..
-instance multiset :: ("term") minus ..
-instance multiset :: ("term") zero ..
+instance multiset :: (type) plus ..
+instance multiset :: (type) minus ..
+instance multiset :: (type) zero ..
 
 defs (overloaded)
   union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
@@ -114,7 +114,7 @@
 
 theorems union_ac = union_assoc union_commute union_lcomm
 
-instance multiset :: ("term") plus_ac0
+instance multiset :: (type) plus_ac0
   apply intro_classes
     apply (rule union_commute)
    apply (rule union_assoc)
@@ -660,7 +660,7 @@
 
 subsubsection {* Partial-order properties *}
 
-instance multiset :: ("term") ord ..
+instance multiset :: (type) ord ..
 
 defs (overloaded)
   less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}"