# HG changeset patch
# User wenzelm
# Date 1204199791 -3600
# Node ID 038baad81209c2183e8adeaf84bca65fb219c0dd
# Parent  11e338832c31dd964fa1e4a24bc5896c5c3e1faa
tuned syntax declaration;

diff -r 11e338832c31 -r 038baad81209 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Feb 28 12:56:30 2008 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Feb 28 12:56:31 2008 +0100
@@ -81,7 +81,7 @@
 
 text {* Multiset Enumeration *}
 syntax
-  "@multiset" :: "args => 'a multiset"    ("{#(_)#}")
+  "_multiset" :: "args => 'a multiset"    ("{#(_)#}")
 translations
   "{#x, xs#}" == "{#x#} + {#xs#}"
   "{#x#}" == "CONST single x"