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