| changeset 6003 | b382568901f6 |
| parent 5960 | 2bebd0d0a961 |
| child 6013 | 6da9ae6d40f5 |
--- a/src/Pure/Isar/outer_parse.ML Tue Dec 01 14:47:26 1998 +0100 +++ b/src/Pure/Isar/outer_parse.ML Tue Dec 01 14:47:52 1998 +0100 @@ -127,7 +127,7 @@ (* enumerations *) -fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- scan) >> op ::; +fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- !!! scan) >> op ::; fun enum sep scan = enum1 sep scan || Scan.succeed []; fun list1 scan = enum1 "," scan;