src/HOL/Library/Multiset.thy

--- a/src/HOL/Library/Multiset.thy	Fri Oct 12 15:08:29 2012 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Oct 12 18:58:20 2012 +0200
@@ -12,7 +12,7 @@
 
 definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}"
 
-typedef (open) 'a multiset = "multiset :: ('a => nat) set"
+typedef 'a multiset = "multiset :: ('a => nat) set"
   morphisms count Abs_multiset
   unfolding multiset_def
 proof