changeset 35351 | 7425aece4ee3 |
parent 35222 | 4f1fba00f66d |
child 35415 | 1810b1ade437 |
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Wed Feb 24 07:06:39 2010 -0800 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Wed Feb 24 20:37:01 2010 +0100 @@ -296,7 +296,7 @@ val quotspec_parser = OuterParse.and_list1 ((OuterParse.type_args -- OuterParse.binding) -- - OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- + OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- (OuterParse.$$$ "/" |-- OuterParse.term)) val _ = OuterKeyword.keyword "/"