src/HOL/Import/hol4rews.ML

     val defmaps = mk (HOL4DefMaps.get thy);
 	fun new_name internal isa =
 	    if internal
 	    then
 		let
-		    val paths = NameSpace.unpack isa
+		    val paths = NameSpace.explode isa
 		    val i = Library.drop(length paths - 2,paths)
 		in
 		    case i of
 			[seg,con] => output_thy ^ "." ^ seg ^ "." ^ con
 		      | _ => error "hol4rews.dump internal error"

 		then ()
 		else out "\n\n"
 
 	fun gen2replay in_thy out_thy s = 
 	    let
-		val ss = NameSpace.unpack s
+		val ss = NameSpace.explode s
 	    in
 		if (hd ss = in_thy) then 
-		    NameSpace.pack (out_thy::(tl ss))
+		    NameSpace.implode (out_thy::(tl ss))
 		else
 		    s
 	    end 
 
 	val _ = if null mapped