| changeset 25999 | f8bcd311d501 |
| parent 25795 | 216c8e70d804 |
| child 27384 | bbb68fea688f |
--- a/src/Pure/Isar/outer_parse.ML Mon Jan 28 18:18:19 2008 +0100 +++ b/src/Pure/Isar/outer_parse.ML Mon Jan 28 22:27:19 2008 +0100 @@ -185,7 +185,7 @@ (* enumerations *) -fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- !!! scan) >> op ::; +fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan); fun enum sep scan = enum1 sep scan || Scan.succeed []; fun list1 scan = enum1 "," scan;