changeset 45343 | 873e9c0ca37d |
parent 45129 | 1fce03e3e8ad |
child 45605 | a89b4bc311a5 |
--- 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|}"