enum: !!! after seperator;
authorwenzelm
Tue, 01 Dec 1998 14:47:52 +0100
changeset 6003 b382568901f6
parent 6002 c1f28f8ec72c
child 6004 47705248cf80
enum: !!! after seperator;
src/Pure/Isar/outer_parse.ML
--- 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;