| changeset 42287 | d98eb048a2e4 |
| parent 40800 | 330eb65c9469 |
| child 42297 | 140f283266b7 |
--- a/src/Pure/Isar/parse.ML Fri Apr 08 14:05:31 2011 +0200 +++ b/src/Pure/Isar/parse.ML Fri Apr 08 14:20:57 2011 +0200 @@ -305,7 +305,7 @@ val fixes = and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) || - params >> map Syntax.no_syn) >> flat; + params >> map (fn (x, y) => (x, y, NoSyn))) >> flat; val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) []; val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) [];