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 []