# HG changeset patch
# User wenzelm
# Date 912520072 -3600
# Node ID b382568901f61433d4a049769d90af04a92ff538
# Parent  c1f28f8ec72c8a0d8df5ea3105d3b3531712d909
enum: !!! after seperator;

diff -r c1f28f8ec72c -r b382568901f6 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;