src/Pure/Syntax/lexicon.ML

   val display_token: token -> string
   val matching_tokens: token * token -> bool
   val token_assoc: (token option * 'a list) list * token -> 'a list
   val valued_token: token -> bool
   val predef_term: string -> token option
-  val tokenize: lexicon -> bool -> string -> token list
+  val tokenize: lexicon -> bool -> string list -> token list
   end;
 
 structure Lexicon : LEXICON =
 struct
 

 
 
 
 (** tokenize **)
 
-fun tokenize lex xids str =
+fun tokenize lex xids chs =
   let
     val scan_xid =
       if xids then $$ "_" ^^ scan_id || scan_id
       else scan_id;
 

           else
             (case max_of scan_lit scan_val chs of
               (None, _) => error ("Lexical error at: " ^ quote (implode chs))
             | (Some (tk, s), chs') => scan (tk s :: rev_toks, chs'));
   in
-    scan ([], explode str)
+    scan ([], chs)
   end;
 
 
 
 (** scan variables **)