src/HOL/IOA/NTP/Multiset.thy

 
   multiset :: (term) term
 
 consts
 
-  "{|}"  :: "'a multiset"                        ("{|}")
-  addm   :: "['a multiset, 'a] => 'a multiset"
-  delm   :: "['a multiset, 'a] => 'a multiset"
-  countm :: "['a multiset, 'a => bool] => nat"
-  count  :: "['a multiset, 'a] => nat"
+  "{|}"  :: 'a multiset                        ("{|}")
+  addm   :: ['a multiset, 'a] => 'a multiset
+  delm   :: ['a multiset, 'a] => 'a multiset
+  countm :: ['a multiset, 'a => bool] => nat
+  count  :: ['a multiset, 'a] => nat
 
 rules
 
 delm_empty_def
   "delm {|} x = {|}"