equal
deleted
inserted
replaced
320 >> (fn (xs, T) => map (rpair T) xs); |
320 >> (fn (xs, T) => map (rpair T) xs); |
321 |
321 |
322 val simple_fixes = and_list1 params >> flat; |
322 val simple_fixes = and_list1 params >> flat; |
323 |
323 |
324 val fixes = |
324 val fixes = |
325 and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) || |
325 and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1) || |
326 params >> map (fn (x, y) => (x, y, NoSyn))) >> flat; |
326 params >> map (fn (x, y) => (x, y, NoSyn))) >> flat; |
327 |
327 |
328 val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) []; |
328 val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) []; |
329 val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) []; |
329 val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) []; |
330 |
330 |