# HG changeset patch
# User wenzelm
# Date 850218937 -3600
# Node ID 963285471dc5bcb85800f31a80a52aca3389f8ee
# Parent  4744b27cdf895f6c61cd22dcec959d47d0294a56
tokenize: no gets exploded char list;

diff -r 4744b27cdf89 -r 963285471dc5 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Dec 10 12:55:00 1996 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Tue Dec 10 12:55:37 1996 +0100
@@ -77,7 +77,7 @@
   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 =
@@ -372,7 +372,7 @@
 
 (** tokenize **)
 
-fun tokenize lex xids str =
+fun tokenize lex xids chs =
   let
     val scan_xid =
       if xids then $$ "_" ^^ scan_id || scan_id
@@ -409,7 +409,7 @@
               (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;