src/Pure/Syntax/simple_syntax.ML
changeset 25999 f8bcd311d501
parent 24487 e92b74b3a254
child 27732 8dbf5761a24a
--- a/src/Pure/Syntax/simple_syntax.ML	Mon Jan 28 18:18:19 2008 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML	Mon Jan 28 22:27:19 2008 +0100
@@ -44,8 +44,8 @@
 (* basic scanners *)
 
 fun $$ s = Scan.some (fn Lexicon.Token s' => if s = s' then SOME s else NONE | _ => NONE);
-fun enum1 s scan = scan -- Scan.repeat ($$ s |-- scan) >> op ::;
-fun enum2 s scan = scan -- Scan.repeat1 ($$ s |-- scan) >> op ::;
+fun enum1 s scan = scan ::: Scan.repeat ($$ s |-- scan);
+fun enum2 s scan = scan ::: Scan.repeat1 ($$ s |-- scan);
 
 val tfree = Scan.some (fn Lexicon.TFreeSy s => SOME s | _ => NONE);
 val ident = Scan.some (fn Lexicon.IdentSy s => SOME s | _ => NONE);