enum: !!! after seperator;
authorwenzelm
Tue Dec 01 14:47:52 1998 +0100 (1998-12-01)
changeset 6003b382568901f6
parent 6002 c1f28f8ec72c
child 6004 47705248cf80
enum: !!! after seperator;
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Tue Dec 01 14:47:26 1998 +0100
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Tue Dec 01 14:47:52 1998 +0100
     1.3 @@ -127,7 +127,7 @@
     1.4  
     1.5  (* enumerations *)
     1.6  
     1.7 -fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- scan) >> op ::;
     1.8 +fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- !!! scan) >> op ::;
     1.9  fun enum sep scan = enum1 sep scan || Scan.succeed [];
    1.10  
    1.11  fun list1 scan = enum1 "," scan;