changeset 205 | 2a803a1556d5 |
parent 203 | 7384115df9fd |
child 207 | 18d7d9dc75cb |
child 212 | ca9eae5bd871 |
--- a/QuotMain.thy Tue Oct 27 14:15:40 2009 +0100 +++ b/QuotMain.thy Tue Oct 27 14:46:38 2009 +0100 @@ -152,7 +152,7 @@ ML {* val quot_def_parser = (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- - ((OuterParse.list1 OuterParse.binding) --| OuterParse.$$$ ")")) -- + ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) -- (OuterParse.binding -- Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec)