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