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