# HG changeset patch
# User wenzelm
# Date 918059213 -3600
# Node ID 58e9f980bd4f2e208949ce95a8f4c86d82aa8ea0
# Parent  7d2204fcc1e58bd0d2476c4c9eeeb877b19b43c6
tokenize: get exploded args;

diff -r 7d2204fcc1e5 -r 58e9f980bd4f src/Pure/Thy/thy_scan.ML
--- a/src/Pure/Thy/thy_scan.ML	Wed Feb 03 17:26:27 1999 +0100
+++ b/src/Pure/Thy/thy_scan.ML	Wed Feb 03 17:26:53 1999 +0100
@@ -13,7 +13,7 @@
   datatype token_kind =
     Keyword | Ident | LongIdent | Var | TypeVar | Nat | String | Verbatim | Ignore | EOF
   val name_of_kind: token_kind -> string
-  val tokenize: Scan.lexicon -> string -> (token_kind * string * int) list
+  val tokenize: Scan.lexicon -> string list -> (token_kind * string * int) list
 end;
 
 structure ThyScan: THY_SCAN =
@@ -138,9 +138,8 @@
 
 (* tokenize *)
 
-fun tokenize lex str =
+fun tokenize lex chs =
   let
-    val chs = explode str;	(*sic!*)
     val scan_toks = Scan.repeat (scan_token lex);
     val ignore = fn (Ignore, _, _) => true | _ => false;
   in