diff -r f9d085c2625c -r 05f57309170c src/HOL/Import/xmlconv.ML
--- a/src/HOL/Import/xmlconv.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Import/xmlconv.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -243,12 +243,12 @@
     ) e
 
 
-fun to_file f output fname x = File.write (Path.unpack fname) (f (output x))
+fun to_file f output fname x = File.write (Path.explode fname) (f (output x))
  
 fun from_file f input fname = 
     let
 	val _ = writeln "read_from_file enter"
-	val s = File.read (Path.unpack fname)
+	val s = File.read (Path.explode fname)
 	val _ = writeln "done: read file"
 	val tree = timeit (fn () => f s)
 	val _ = writeln "done: tree"