# HG changeset patch
# User wenzelm
# Date 1290210806 -3600
# Node ID becf5d5187ccefede360907cb49f7e415a560ee2
# Parent  d86540f6ea0d44d07fd833b38bc1c3d7d2890318
renamed raw "explode" function to "raw_explode" to emphasize its meaning;

diff -r d86540f6ea0d -r becf5d5187cc NEWS
--- a/NEWS	Fri Nov 19 23:48:07 2010 +0100
+++ b/NEWS	Sat Nov 20 00:53:26 2010 +0100
@@ -490,6 +490,10 @@
 
 *** ML ***
 
+* Renamed raw "explode" function to "raw_explode" to emphasize its
+meaning.  Note that internally to Isabelle, Symbol.explode is used in
+almost all situations.
+
 * Discontinued obsolete function sys_error and exception SYS_ERROR.
 See implementation manual for further details on exceptions in
 Isabelle/ML.
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Boogie/Tools/boogie_commands.ML
--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -116,7 +116,7 @@
 end
 
 fun write_list head =
-  map Pretty.str o sort (dict_ord string_ord o pairself explode) #>
+  map Pretty.str o sort (dict_ord string_ord o pairself raw_explode) #>
   Pretty.writeln o Pretty.big_list head
 
 fun parens s = "(" ^ s ^ ")"
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -344,7 +344,7 @@
     | (_, ts') => error (scan_err "unparsed input" ts'))
   end
 
-fun read_int' s = (case read_int (explode s) of (i, []) => SOME i | _ => NONE)
+fun read_int' s = (case read_int (raw_explode s) of (i, []) => SOME i | _ => NONE)
 
 fun $$$ s = Scan.one (fn (_, Token s') => s = s' | _ => false)
 fun str st = Scan.some (fn (_, Token s) => SOME s | _ => NONE) st
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Import/lazy_seq.ML
--- a/src/HOL/Import/lazy_seq.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Import/lazy_seq.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -543,7 +543,7 @@
         F e (getItem s)
     end
 
-fun fromString s = of_list (explode s)
+fun fromString s = of_list (raw_explode s)
 
 end
 
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Import/mono_scan.ML
--- a/src/HOL/Import/mono_scan.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Import/mono_scan.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -233,6 +233,6 @@
 fun this [] = (fn toks => ([], toks))
   | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
 
-fun this_string s = this (explode s) >> K s
+fun this_string s = this (raw_explode s) >> K s
 
 end
\ No newline at end of file
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -501,8 +501,8 @@
 
 fun replacestr x y s =
 let
-  val xl = explode x
-  val yl = explode y
+  val xl = raw_explode x
+  val yl = raw_explode y
   fun isprefix [] ys = true
     | isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false
     | isprefix _ _ = false
@@ -511,7 +511,7 @@
   fun r [] = []
     | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss)
 in
-  implode(r (explode s))
+  implode(r (raw_explode s))
 end
 
 fun protect_factname s = replacestr "." "_dot_" s
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Import/scan.ML
--- a/src/HOL/Import/scan.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Import/scan.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -213,7 +213,7 @@
 fun this [] = (fn toks => ([], toks))
   | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
 
-fun this_string s = this (explode s) >> K s
+fun this_string s = this (raw_explode s) >> K s
 
 end
 
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Import/seq.ML
--- a/src/HOL/Import/seq.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Import/seq.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -94,6 +94,6 @@
 open Extended
 
 val fromList = I
-val fromString = explode
+val fromString = raw_explode
 
 end
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -79,7 +79,7 @@
    val z = pow10(~ e) */ y +/ rat_1
    val k = int_of_rat (round_rat(pow10 d */ z))
   in (if x </ rat_0 then "-0." else "0.") ^
-     implode(tl(explode(string_of_int k))) ^
+     implode(tl(raw_explode(string_of_int k))) ^
      (if e = 0 then "" else "e"^string_of_int e)
   end
 end;
@@ -558,7 +558,7 @@
     >> (fn (h, x) => h */ pow10 (int_of_rat x));
 
  fun mkparser p s =
-  let val (x,rst) = p (explode s)
+  let val (x,rst) = p (raw_explode s)
   in if null rst then x
      else error "mkparser: unparsed input"
   end;;
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -444,7 +444,7 @@
     val (prover_name, _) = get_prover ctxt args
     val timeout =
       AList.lookup (op =) args minimize_timeoutK
-      |> Option.map (fst o read_int o explode)
+      |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)
       |> the_default 5
     val params = Sledgehammer_Isar.default_params ctxt
       [("verbose", "true"),
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -723,7 +723,7 @@
       | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i))
       | reindex dt = dt;
 
-    fun strip_suffix i s = implode (List.take (explode s, size s - i));
+    fun strip_suffix i s = implode (List.take (raw_explode s, size s - i));  (* FIXME Symbol.explode (?) *)
 
     (** strips the "_Rep" in type names *)
     fun strip_nth_name i s =
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Sat Nov 20 00:53:26 2010 +0100
@@ -389,7 +389,7 @@
 ML {*
 fun dBtype_of_typ (Type ("fun", [T, U])) =
       @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
-  | dBtype_of_typ (TFree (s, _)) = (case explode s of
+  | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
         ["'", a] => @{code Atom} (@{code nat} (ord a - 97))
       | _ => error "dBtype_of_typ: variable name")
   | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
@@ -458,7 +458,7 @@
 
 fun dBtype_of_typ (Type ("fun", [T, U])) =
       Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)
-  | dBtype_of_typ (TFree (s, _)) = (case explode s of
+  | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
         ["'", a] => Norm.Atom (nat_of_int (ord a - 97))
       | _ => error "dBtype_of_typ: variable name")
   | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -321,7 +321,7 @@
   fst o Scan.finite Symbol.stopper
             (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
                             (Scan.repeat1 parse_line)))
-  o explode o strip_spaces_except_between_ident_chars
+  o raw_explode o strip_spaces_except_between_ident_chars
 
 fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen
 fun clean_up_dependencies _ [] = []
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -48,7 +48,7 @@
 
 fun make_tnames Ts =
   let
-    fun type_name (TFree (name, _)) = implode (tl (explode name))
+    fun type_name (TFree (name, _)) = implode (tl (raw_explode name))  (* FIXME Symbol.explode (?) *)
       | type_name (Type (name, _)) = 
           let val name' = Long_Name.base_name name
           in if Syntax.is_identifier name' then name' else "x" end;
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Function/size.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -71,7 +71,7 @@
     val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
       map (fn T as TFree (s, _) =>
         let
-          val name = "f" ^ implode (tl (explode s));
+          val name = "f" ^ implode (tl (raw_explode s));  (* FIXME Symbol.explode (?) *)
           val U = T --> HOLogic.natT
         in
           (((s, Free (name, U)), U), name)
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -908,7 +908,7 @@
                                 raise SYNTAX ("Kodkod.extract_instance",
                                               "ill-formed Kodkodi output"))
                             (parse_instance new_kodkodi)))
-  o strip_blanks o explode
+  o strip_blanks o raw_explode
 
 val problem_marker = "*** PROBLEM "
 val outcome_marker = "---OUTCOME---\n"
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -120,7 +120,7 @@
   | NONE => (Unsynchronized.change pool (cons (T, [j])); 1)
 fun atom_suffix s =
   nat_subscript
-  #> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
+  #> (s <> "" andalso Symbol.is_ascii_digit (List.last (raw_explode s)))  (* FIXME Symbol.explode (?) *)
      ? prefix "\<^isub>,"
 fun nth_atom_name thy atomss pool prefix T j =
   let
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -240,7 +240,7 @@
 val parse_time_option = Sledgehammer_Util.parse_time_option
 val string_from_time = Sledgehammer_Util.string_from_time
 
-val i_subscript = implode o map (prefix "\<^isub>") o explode
+val i_subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
 fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
 fun nat_subscript n =
   let val s = signed_string_of_int n in
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/SMT/z3_model.ML
--- a/src/HOL/Tools/SMT/z3_model.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_model.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -38,7 +38,7 @@
   (fn sign => nat_num >> sign))
 
 val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
-  member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
+  member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
 val name = spaced (Scan.many1 is_char >> implode)
 
 fun $$$ s = spaced (Scan.this_string s)
@@ -68,7 +68,7 @@
   Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair [])))
 
 fun read_cex ls =
-  maps (cons "\n" o explode) ls
+  maps (cons "\n" o raw_explode) ls
   |> try (fst o Scan.finite Symbol.stopper cex)
   |> the_default []
 
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/SMT/z3_proof_parser.ML
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -256,7 +256,7 @@
 
 fun parse_line _ _ (st as ((SOME _, _), _)) = st
   | parse_line scan line ((_, line_no), cx) =
-      let val st = ((line_no, cx), explode line)
+      let val st = ((line_no, cx), raw_explode line)
       in
         (case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of
           (SOME r, ((_, cx'), _)) => ((r, line_no+1), cx')
@@ -299,7 +299,7 @@
   (fn sign => nat_num >> sign)) st
 
 val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
-  member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
+  member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
 fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st
 
 fun sym st =
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -313,7 +313,7 @@
         val digit = Scan.one Symbol.is_ascii_digit;
         val num3 = as_num (digit ::: digit ::: (digit >> single));
         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
-        val as_time = Scan.read Symbol.stopper time o explode
+        val as_time = Scan.read Symbol.stopper time o raw_explode
       in (output, as_time t) end;
     fun run_on probfile =
       case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -81,7 +81,7 @@
 val extract_clause_formula_relation =
   Substring.full #> Substring.position set_ClauseFormulaRelationN
   #> snd #> Substring.position "." #> fst #> Substring.string
-  #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
+  #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
   #> fst
 
 fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names =
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -51,7 +51,7 @@
          end
 
 val has_junk =
-  exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o explode
+  exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
 
 fun parse_time_option _ "none" = NONE
   | parse_time_option name s =
@@ -66,7 +66,7 @@
 fun string_from_time t =
   string_of_real (0.01 * Real.fromInt (Time.toMilliseconds t div 10)) ^ " s"
 
-val subscript = implode o map (prefix "\<^isub>") o explode
+val subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
 fun nat_subscript n =
   n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
 
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/hologic.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -598,7 +598,7 @@
 
 val stringT = listT charT;
 
-val mk_string = mk_list charT o map (mk_char o ord) o explode;
+val mk_string = mk_list charT o map (mk_char o ord) o raw_explode;
 val dest_string = implode o map (chr o dest_char) o dest_list;
 
 
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/refute.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -2955,7 +2955,7 @@
     (* string -> string *)
     fun strip_leading_quote s =
       (implode o (fn [] => [] | x::xs => if x="'" then xs else x::xs)
-        o explode) s
+        o raw_explode) s  (* FIXME Symbol.explode (?) *)
     (* Term.typ -> string *)
     fun string_of_typ (Type (s, _)) = s
       | string_of_typ (TFree (x, _)) = strip_leading_quote x
diff -r d86540f6ea0d -r becf5d5187cc src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Tools/string_syntax.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -32,7 +32,7 @@
     Syntax.Appl [Syntax.Constant @{const_syntax Char}, mk_nib (ord s div 16), mk_nib (ord s mod 16)]
   else error ("Non-ASCII symbol: " ^ quote s);
 
-val specials = explode "\\\"`'";
+val specials = raw_explode "\\\"`'";
 
 fun dest_chr c1 c2 =
   let val c = chr (dest_nib c1 * 16 + dest_nib c2) in
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/General/path.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -73,9 +73,9 @@
 
 val current = Path [];
 val root = Path [Root ""];
-fun named_root s = Path [root_elem (explode s)];
-fun basic s = Path [basic_elem (explode s)];
-fun variable s = Path [variable_elem (explode s)];
+fun named_root s = Path [root_elem (raw_explode s)];
+fun basic s = Path [basic_elem (raw_explode s)];
+fun variable s = Path [variable_elem (raw_explode s)];
 val parent = Path [Parent];
 
 fun is_absolute (Path xs) =
@@ -128,7 +128,7 @@
   | explode_elem "~" = Variable "HOME"
   | explode_elem "~~" = Variable "ISABELLE_HOME"
   | explode_elem s =
-      (case explode s of
+      (case raw_explode s of
         "$" :: cs => variable_elem cs
       | cs => basic_elem cs);
 
@@ -143,7 +143,7 @@
       (0, es) => ([], es)
     | (1, es) => ([Root ""], es)
     | (_, []) => ([Root ""], [])
-    | (_, e :: es) => ([root_elem (explode e)], es))
+    | (_, e :: es) => ([root_elem (raw_explode e)], es))
   in Path (norm (explode_elems raw_elems @ roots)) end;
 
 end;
@@ -161,7 +161,7 @@
   | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
 
 val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
-  (case take_suffix (fn c => c <> ".") (explode s) of
+  (case take_suffix (fn c => c <> ".") (raw_explode s) of
     ([], _) => (Path [Basic s], "")
   | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
 
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/General/scan.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -154,7 +154,7 @@
           if (y: string) = x then drop_prefix ys xs else raise FAIL NONE;
   in (ys, drop_prefix ys xs) end;
 
-fun this_string s = this (explode s) >> K s;  (*primitive string -- no symbols here!*)
+fun this_string s = this (raw_explode s) >> K s;  (*primitive string -- no symbols here!*)
 
 fun many _ [] = raise MORE NONE
   | many pred (lst as x :: xs) =
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/General/source.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -107,7 +107,7 @@
 
 (* string source *)
 
-val of_string = of_list o explode;
+val of_string = of_list o raw_explode;
 
 fun of_string_limited limit str =
   make_source [] (Substring.full str) default_prompt
@@ -127,14 +127,14 @@
         NONE => []
       | SOME 0 => []
       | SOME _ => TextIO.input instream :: slurp ());
-  in maps explode (slurp ()) end;
+  in maps raw_explode (slurp ()) end;
 
 fun tty in_stream = make_source [] () default_prompt (fn prompt => fn () =>
   let val input = slurp_input in_stream in
     if exists (fn c => c = "\n") input then (input, ())
     else
       (case (Output.prompt prompt; TextIO.inputLine in_stream) of
-        SOME line => (input @ explode line, ())
+        SOME line => (input @ raw_explode line, ())
       | NONE => (input, ()))
   end);
 
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/General/symbol.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -188,7 +188,7 @@
           | enc ([], d :: ds) = raw2 d :: encode ds
           | enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds;
       in
-        if exists_string (not o raw_chr) str then implode (encode (explode str))
+        if exists_string (not o raw_chr) str then implode (encode (raw_explode str))
         else raw0 str
       end;
 
@@ -215,7 +215,7 @@
 fun decode_raw s =
   if not (is_raw s) then error (malformed_msg s)
   else if String.isPrefix "\\<^raw:" s then String.substring (s, 7, size s - 8)
-  else chr (#1 (Library.read_int (explode (String.substring (s, 6, size s - 7)))));
+  else chr (#1 (Library.read_int (raw_explode (String.substring (s, 6, size s - 7)))));
 
 
 (* symbol variants *)
@@ -470,7 +470,7 @@
 in
 
 fun sym_explode str =
-  let val chs = explode str in
+  let val chs = raw_explode str in
     if no_explode chs then chs
     else Source.exhaust (source (Source.of_list chs))
   end;
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/General/xml.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -158,7 +158,7 @@
 val parse_comments =
   blanks -- Scan.repeat (parse_comment -- blanks >> K ()) >> K ();
 
-val parse_string = Scan.read Symbol.stopper parse_chars o explode;
+val parse_string = Scan.read Symbol.stopper parse_chars o raw_explode;
 
 fun parse_content xs =
   (parse_optional_text @@@
@@ -184,7 +184,7 @@
 
 fun parse s =
   (case Scan.finite Symbol.stopper (Scan.error (!! (err "Malformed element")
-      (blanks |-- parse_document --| blanks))) (explode s) of
+      (blanks |-- parse_document --| blanks))) (raw_explode s) of
     (x, []) => x
   | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
 
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/Isar/class.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -477,7 +477,7 @@
         --| junk))
       ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
   in
-    explode #> scan_valids #> implode
+    raw_explode #> scan_valids #> implode
   end;
 
 val type_name = sanitize_name o Long_Name.base_name;
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/Isar/token.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -265,7 +265,7 @@
 
 (* scan symbolic idents *)
 
-val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
+val is_sym_char = member (op =) (raw_explode "!#$%&*+-/<=>?@^_|~");
 
 val scan_symid =
   Scan.many1 (is_sym_char o Symbol_Pos.symbol) ||
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -29,6 +29,7 @@
 val _ = PolyML.Compiler.forgetValue "foldl";
 val _ = PolyML.Compiler.forgetValue "foldr";
 val _ = PolyML.Compiler.forgetValue "print";
+val _ = PolyML.Compiler.forgetValue "explode";
 
 
 (* Compiler options *)
@@ -48,7 +49,7 @@
 
 val ord = SML90.ord;
 val chr = SML90.chr;
-val explode = SML90.explode;
+val raw_explode = SML90.explode;
 val implode = SML90.implode;
 
 
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -30,9 +30,9 @@
 
 (* restore old-style character / string functions *)
 
-val ord     = mk_int o SML90.ord;
-val chr     = SML90.chr o dest_int;
-val explode = SML90.explode;
+val ord = mk_int o SML90.ord;
+val chr = SML90.chr o dest_int;
+val raw_explode = SML90.explode;
 val implode = SML90.implode;
 
 
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/ML/ml_lex.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -149,7 +149,7 @@
   "sharing", "sig", "signature", "struct", "structure", "then", "type",
   "val", "where", "while", "with", "withtype"];
 
-val lex = Scan.make_lexicon (map explode keywords);
+val lex = Scan.make_lexicon (map raw_explode keywords);
 fun scan_keyword x = Scan.literal lex x;
 
 
@@ -166,7 +166,7 @@
   Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) -- scan_letdigs >> op ::;
 
 val scan_symbolic =
-  Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);
+  Scan.many1 (member (op =) (raw_explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);
 
 in
 
@@ -211,7 +211,7 @@
 local
 
 val scan_escape =
-  Scan.one (member (op =) (explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
+  Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
   $$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) ||
   Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
     Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/Proof/extraction.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -68,7 +68,7 @@
   | rlz_proc _ = NONE;
 
 val unpack_ixn = apfst implode o apsnd (fst o read_int o tl) o
-  take_prefix (fn s => s <> ":") o explode;
+  take_prefix (fn s => s <> ":") o raw_explode;
 
 type rules =
   {next: int, rs: ((term * term) list * (term * term)) list,
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/codegen.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -355,7 +355,7 @@
   Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x;
 
 fun dest_sym s =
-  (case split_last (snd (take_prefix (fn c => c = "\\") (explode s))) of
+  (case split_last (snd (take_prefix (fn c => c = "\\") (raw_explode s))) of
     ("<" :: "^" :: xs, ">") => (true, implode xs)
   | ("<" :: xs, ">") => (false, implode xs)
   | _ => raise Fail "dest_sym");
@@ -374,7 +374,7 @@
         | (ys, zs) => implode ys :: check_str zs);
     val s' = space_implode "_" (maps (check_str o Symbol.explode) (Long_Name.explode s))
   in
-    if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
+    if Symbol.is_ascii_letter (hd (raw_explode s')) then s' else "id_" ^ s'
   end;
 
 fun mk_long_id (p as (tab, used)) module s =
@@ -826,7 +826,7 @@
 
 (**** Reflection ****)
 
-val strip_tname = implode o tl o explode;
+val strip_tname = implode o tl o raw_explode;
 
 fun pretty_list xs = Pretty.block (str "[" ::
   flat (separate [str ",", Pretty.brk 1] (map single xs)) @
@@ -962,7 +962,7 @@
 val _ = List.app Keyword.keyword ["attach", "file", "contains"];
 
 fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ")
-  (snd (take_prefix (fn c => c = "\n" orelse c = " ") (explode s))))) ^ "\n";
+  (snd (take_prefix (fn c => c = "\n" orelse c = " ") (raw_explode s))))) ^ "\n";
 
 val parse_attach = Scan.repeat (Parse.$$$ "attach" |--
   Scan.optional (Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")") "" --
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/library.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -669,7 +669,7 @@
 
 val read_int = read_radix_int 10;
 
-fun oct_char s = chr (#1 (read_radix_int 8 (explode s)));
+fun oct_char s = chr (#1 (read_radix_int 8 (raw_explode s)));
 
 
 
diff -r d86540f6ea0d -r becf5d5187cc src/Pure/name.ML
--- a/src/Pure/name.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/name.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -166,7 +166,7 @@
           if is_valid x then x :: xs
           else
             (case Symbol.decode x of
-              Symbol.Sym name => "_" :: explode name @ sep xs
+              Symbol.Sym name => "_" :: raw_explode name @ sep xs
             | _ => sep xs);
         fun upper_lower cs =
           if upper then nth_map 0 Symbol.to_ascii_upper cs
diff -r d86540f6ea0d -r becf5d5187cc src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Tools/Code/code_ml.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -679,7 +679,7 @@
   fun chr i =
     let
       val xs = string_of_int i;
-      val ys = replicate_string (3 - length (explode xs)) "0";
+      val ys = replicate_string (3 - length (raw_explode xs)) "0";
     in "\\" ^ ys ^ xs end;
   fun char_ocaml c =
     let
diff -r d86540f6ea0d -r becf5d5187cc src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Tools/Code/code_printer.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -173,8 +173,8 @@
  of SOME name' => name'
   | NONE => error ("Invalid name in context: " ^ quote name);
 
-val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
-val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
+val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
+val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;
 
 fun aux_params vars lhss =
   let
diff -r d86540f6ea0d -r becf5d5187cc src/Tools/IsaPlanner/rw_tools.ML
--- a/src/Tools/IsaPlanner/rw_tools.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Tools/IsaPlanner/rw_tools.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -20,10 +20,10 @@
 construction/definition. *)
 (*
 fun dest_fake_bound_name n = 
-    case (explode n) of 
+    case (raw_explode n) of   (* FIXME Symbol.explode (?) *)
       (":" :: realchars) => implode realchars
     | _ => n; *)
-fun is_fake_bound_name n = (hd (explode n) = ":");
+fun is_fake_bound_name n = (hd (raw_explode n) = ":");  (* FIXME Symbol.explode (?) *)
 fun mk_fake_bound_name n = ":b_" ^ n;
 
 
@@ -31,20 +31,20 @@
 (* fake free variable names for local meta variables - these work
 as placeholders. *)
 fun dest_fake_fix_name n = 
-    case (explode n) of 
+    case (raw_explode n) of  (* FIXME Symbol.explode (?) *)
       ("@" :: realchars) => implode realchars
     | _ => n;
-fun is_fake_fix_name n = (hd (explode n) = "@");
+fun is_fake_fix_name n = (hd (raw_explode n) = "@");  (* FIXME Symbol.explode (?) *)
 fun mk_fake_fix_name n = "@" ^ n;
 
 
 
 (* fake free variable names for meta level bound variables *)
 fun dest_fake_all_name n = 
-    case (explode n) of 
+    case (raw_explode n) of   (* FIXME Symbol.explode (?) *)
       ("+" :: realchars) => implode realchars
     | _ => n;
-fun is_fake_all_name n = (hd (explode n) = "+");
+fun is_fake_all_name n = (hd (raw_explode n) = "+");  (* FIXME Symbol.explode (?) *)
 fun mk_fake_all_name n = "+" ^ n;
 
 
diff -r d86540f6ea0d -r becf5d5187cc src/Tools/WWW_Find/unicode_symbols.ML
--- a/src/Tools/WWW_Find/unicode_symbols.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -82,7 +82,7 @@
   -- Scan.many (not o Symbol.is_ascii_blank o Symbol_Pos.symbol)
   >> (token AsciiSymbol o op ::);
 
-fun not_contains xs c = not (member (op =) (explode xs) (Symbol_Pos.symbol c));
+fun not_contains xs c = not (member (op =) (raw_explode xs) (Symbol_Pos.symbol c));
 val scan_comment =
   $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
   >> token Comment;
diff -r d86540f6ea0d -r becf5d5187cc src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Tools/cache_io.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -81,7 +81,7 @@
       File.shell_path cache_path)
 
     fun int_of_string s =
-      (case read_int (explode s) of
+      (case read_int (raw_explode s) of
         (i, []) => i
       | _ => err ())