--- a/src/HOL/Import/hol4rews.ML Sun Mar 08 17:19:15 2009 +0100
+++ b/src/HOL/Import/hol4rews.ML Sun Mar 08 17:26:14 2009 +0100
@@ -495,7 +495,7 @@
if internal
then
let
- val paths = NameSpace.explode isa
+ val paths = Long_Name.explode isa
val i = Library.drop(length paths - 2,paths)
in
case i of
@@ -549,10 +549,10 @@
fun gen2replay in_thy out_thy s =
let
- val ss = NameSpace.explode s
+ val ss = Long_Name.explode s
in
if (hd ss = in_thy) then
- NameSpace.implode (out_thy::(tl ss))
+ Long_Name.implode (out_thy::(tl ss))
else
s
end