diff -r f38dc602a926 -r f8bcd311d501 src/Pure/Syntax/simple_syntax.ML --- 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);