diff -r 7870cf61c4b3 -r 2e487fe9593a src/HOL/Import/xmlconv.ML
--- a/src/HOL/Import/xmlconv.ML	Thu Feb 16 21:15:38 2006 +0100
+++ b/src/HOL/Import/xmlconv.ML	Thu Feb 16 23:30:47 2006 +0100
@@ -57,6 +57,9 @@
 
   val write_to_file: 'a output -> string -> 'a -> unit
   val read_from_file: 'a input -> string -> 'a
+
+  val serialize_to_file : 'a output -> string -> 'a -> unit
+  val deserialize_from_file : 'a input -> string -> 'a
 end;
 
 structure XMLConv : XML_CONV =
@@ -240,14 +243,14 @@
     ) e
 
 
-fun write_to_file output fname x = File.write (Path.unpack fname) (XML.string_of_tree (output x))
+fun to_file f output fname x = File.write (Path.unpack fname) (f (output x))
  
-fun read_from_file input fname = 
+fun from_file f input fname = 
     let
 	val _ = writeln "read_from_file enter"
 	val s = File.read (Path.unpack fname)
 	val _ = writeln "done: read file"
-	val tree = timeit (fn () => XML.tree_of_string s)
+	val tree = timeit (fn () => f s)
 	val _ = writeln "done: tree"
 	val x = timeit (fn () => input tree)
 	val _ = writeln "done: input"
@@ -255,6 +258,12 @@
 	x
     end
 
+fun write_to_file x = to_file XML.string_of_tree x
+fun read_from_file x = timeit (fn () => (writeln "read_from_file"; from_file XML.tree_of_string x))
+
+fun serialize_to_file x = to_file XML.encoded_string_of_tree x
+fun deserialize_from_file x = timeit (fn () => (writeln "deserialize_from_file"; from_file XML.tree_of_encoded_string x))
+
 end;
 
 structure XMLConvOutput =