# HG changeset patch
# User wenzelm
# Date 1320487151 -3600
# Node ID 873e9c0ca37d2d9a62030b6cb297842691ea5dc7
# Parent  5c760e1692b34eb3cf6851ff164c0489d8bd62ac
more conventional syntax const;

diff -r 5c760e1692b3 -r 873e9c0ca37d src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Fri Nov 04 20:16:42 2011 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Sat Nov 05 10:59:11 2011 +0100
@@ -416,7 +416,7 @@
   is "Cons"
 
 syntax
-  "@Insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
+  "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")
 
 translations
   "{|x, xs|}" == "CONST insert_fset x {|xs|}"