diff -r ad90d96c2ec3 -r 43506f0a98ae src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Nov 29 12:25:15 1993 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Mon Nov 29 12:27:29 1993 +0100
@@ -9,6 +9,24 @@
 infix 3 >>;
 infix 0 ||;
 
+signature SCANNER =
+sig
+  exception LEXICAL_ERROR
+  val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
+  val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
+  val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
+  val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
+  val $$ : ''a -> ''a list -> ''a * ''a list
+  val scan_empty: 'a list -> 'b list * 'a list
+  val scan_one: ('a -> bool) -> 'a list -> 'a * 'a list
+  val scan_any: ('a -> bool) -> 'a list -> 'a list * 'a list
+  val scan_any1: ('a -> bool) -> 'a list -> 'a list * 'a list
+  val scan_end: 'a list -> 'b list * 'a list
+  val optional: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
+  val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
+  val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
+end;
+
 signature LEXICON0 =
 sig
   val is_identifier: string -> bool
@@ -19,6 +37,7 @@
 
 signature LEXICON =
 sig
+  include SCANNER
   include LEXICON0
   val is_xid: string -> bool
   val is_tfree: string -> bool
@@ -44,21 +63,6 @@
   val extend_lexicon: lexicon -> string list -> lexicon
   val mk_lexicon: string list -> lexicon
   val tokenize: lexicon -> bool -> string -> token list
-
-  exception LEXICAL_ERROR
-  val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
-  val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
-  val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
-  val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
-  val $$ : ''a -> ''a list -> ''a * ''a list
-  val scan_empty: 'a list -> 'b list * 'a list
-  val scan_one: ('a -> bool) -> 'a list -> 'a * 'a list
-  val scan_any: ('a -> bool) -> 'a list -> 'a list * 'a list
-  val scan_any1: ('a -> bool) -> 'a list -> 'a list * 'a list
-  val scan_end: 'a list -> 'b list * 'a list
-  val optional: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
-  val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
-  val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
 end;
 
 functor LexiconFun(): LEXICON =
@@ -254,7 +258,10 @@
   | scan_one pred (c :: cs) =
       if pred c then (c, cs) else raise LEXICAL_ERROR;
 
-val scan_any = take_prefix;
+fun scan_any _ [] = ([], [])
+  | scan_any pred (chs as c :: cs) =
+      if pred c then apfst (cons c) (scan_any pred cs)
+      else ([], chs);
 
 fun scan_any1 pred = scan_one pred -- scan_any pred >> op ::;