src/HOL/Import/proof_kernel.ML
changeset 40627 becf5d5187cc
parent 39557 fe5722fce758
child 40840 2f97215e79bf
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -501,8 +501,8 @@
     1.4  
     1.5  fun replacestr x y s =
     1.6  let
     1.7 -  val xl = explode x
     1.8 -  val yl = explode y
     1.9 +  val xl = raw_explode x
    1.10 +  val yl = raw_explode y
    1.11    fun isprefix [] ys = true
    1.12      | isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false
    1.13      | isprefix _ _ = false
    1.14 @@ -511,7 +511,7 @@
    1.15    fun r [] = []
    1.16      | r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss)
    1.17  in
    1.18 -  implode(r (explode s))
    1.19 +  implode(r (raw_explode s))
    1.20  end
    1.21  
    1.22  fun protect_factname s = replacestr "." "_dot_" s