| changeset 25999 | f8bcd311d501 |
| parent 25094 | ba43514068fd |
| child 26336 | a0e2b706ce73 |
--- a/src/Pure/Isar/spec_parse.ML Mon Jan 28 18:18:19 2008 +0100 +++ b/src/Pure/Isar/spec_parse.ML Mon Jan 28 22:27:19 2008 +0100 @@ -108,7 +108,7 @@ >> (curry Element.Notes ""); fun plus1_unless test scan = - scan -- Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)) >> op ::; + scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)); val rename = P.name -- Scan.option P.mixfix;