# HG changeset patch
# User wenzelm
# Date 1353943702 -3600
# Node ID ce1f0602f48ee0c02fc5a6d3d4c045a4a714cbcc
# Parent  de77cde5737658374ac3ea4e8c535858f3d64233
clarified status of Legacy_XML_Syntax, despite lack of Proofterm_XML;

diff -r de77cde57376 -r ce1f0602f48e src/Pure/ROOT
--- a/src/Pure/ROOT	Mon Nov 26 16:22:29 2012 +0100
+++ b/src/Pure/ROOT	Mon Nov 26 16:28:22 2012 +0100
@@ -200,7 +200,7 @@
     "Thy/thy_output.ML"
     "Thy/thy_syntax.ML"
     "Tools/named_thms.ML"
-    "Tools/xml_syntax.ML"
+    "Tools/legacy_xml_syntax.ML"
     "assumption.ML"
     "axclass.ML"
     "config.ML"
diff -r de77cde57376 -r ce1f0602f48e src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Nov 26 16:22:29 2012 +0100
+++ b/src/Pure/ROOT.ML	Mon Nov 26 16:28:22 2012 +0100
@@ -283,7 +283,7 @@
 
 use "Tools/named_thms.ML";
 
-use "Tools/xml_syntax.ML";
+use "Tools/legacy_xml_syntax.ML";
 
 
 (* configuration for Proof General *)
diff -r de77cde57376 -r ce1f0602f48e src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon Nov 26 16:22:29 2012 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Mon Nov 26 16:28:22 2012 +0100
@@ -116,17 +116,17 @@
   | xml_of_criterion Elim = XML.Elem (("Elim", []) , [])
   | xml_of_criterion Dest = XML.Elem (("Dest", []) , [])
   | xml_of_criterion Solves = XML.Elem (("Solves", []) , [])
-  | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []) , [XML_Syntax.xml_of_term pat])
-  | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []) , [XML_Syntax.xml_of_term pat]);
+  | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []), [Legacy_XML_Syntax.xml_of_term pat])
+  | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []), [Legacy_XML_Syntax.xml_of_term pat]);
 
 fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name
   | criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro
   | criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim
   | criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest
   | criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves
-  | criterion_of_xml (XML.Elem (("Simp", []) , [tree])) = Simp (XML_Syntax.term_of_xml tree)
-  | criterion_of_xml (XML.Elem (("Pattern", []) , [tree])) = Pattern (XML_Syntax.term_of_xml tree)
-  | criterion_of_xml tree = raise XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
+  | criterion_of_xml (XML.Elem (("Simp", []), [tree])) = Simp (Legacy_XML_Syntax.term_of_xml tree)
+  | criterion_of_xml (XML.Elem (("Pattern", []), [tree])) = Pattern (Legacy_XML_Syntax.term_of_xml tree)
+  | criterion_of_xml tree = raise Legacy_XML_Syntax.XML ("criterion_of_xml: bad tree", tree);
 
 fun xml_of_query {goal = NONE, limit, rem_dups, criteria} =
       let
@@ -149,7 +149,7 @@
       in
         {goal = NONE, limit = limit, rem_dups = rem_dups, criteria = criteria}
       end
-  | query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
+  | query_of_xml tree = raise Legacy_XML_Syntax.XML ("query_of_xml: bad tree", tree);
 
 
 
@@ -167,7 +167,7 @@
 
 fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal"
   | xml_of_theorem (External (fact_ref, prop)) =
-      XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop]);
+      XML.Elem (fact_ref_markup fact_ref ("External", []), [Legacy_XML_Syntax.xml_of_term prop]);
 
 fun theorem_of_xml (XML.Elem (("External", properties), [tree])) =
       let
@@ -177,9 +177,9 @@
           Option.map (single o Facts.Single o Markup.parse_int)
             (Properties.get properties "index");
       in
-        External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
+        External (Facts.Named ((name, pos), intvs_opt), Legacy_XML_Syntax.term_of_xml tree)
       end
-  | theorem_of_xml tree = raise XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
+  | theorem_of_xml tree = raise Legacy_XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
 
 fun xml_of_result (opt_found, theorems) =
   let
@@ -192,7 +192,7 @@
 fun result_of_xml (XML.Elem (("Result", properties), body)) =
       (Properties.get properties "found" |> Option.map Markup.parse_int,
        XML.Decode.list (theorem_of_xml o the_single) body)
-  | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
+  | result_of_xml tree = raise Legacy_XML_Syntax.XML ("result_of_xml: bad tree", tree);
 
 fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
   | prop_of (External (_, prop)) = prop;
diff -r de77cde57376 -r ce1f0602f48e src/Pure/Tools/legacy_xml_syntax.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/legacy_xml_syntax.ML	Mon Nov 26 16:28:22 2012 +0100
@@ -0,0 +1,173 @@
+(*  Title:      Pure/Tools/legacy_xml_syntax.ML
+    Author:     Stefan Berghofer, TU Muenchen
+
+Input and output of types, terms, and proofs in XML format.
+See isabelle.xsd for a description of the syntax.
+
+Legacy module, see Pure/term_xml.ML etc.
+*)
+
+signature LEGACY_XML_SYNTAX =
+sig
+  val xml_of_type: typ -> XML.tree
+  val xml_of_term: term -> XML.tree
+  val xml_of_proof: Proofterm.proof -> XML.tree
+  val write_to_file: Path.T -> string -> XML.tree -> unit
+  exception XML of string * XML.tree
+  val type_of_xml: XML.tree -> typ
+  val term_of_xml: XML.tree -> term
+  val proof_of_xml: XML.tree -> Proofterm.proof
+end;
+
+structure Legacy_XML_Syntax : LEGACY_XML_SYNTAX =
+struct
+
+(**** XML output ****)
+
+fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
+
+fun xml_of_type (TVar ((s, i), S)) =
+      XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
+        map xml_of_class S)
+  | xml_of_type (TFree (s, S)) =
+      XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
+  | xml_of_type (Type (s, Ts)) =
+      XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
+
+fun xml_of_term (Bound i) =
+      XML.Elem (("Bound", [("index", string_of_int i)]), [])
+  | xml_of_term (Free (s, T)) =
+      XML.Elem (("Free", [("name", s)]), [xml_of_type T])
+  | xml_of_term (Var ((s, i), T)) =
+      XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
+        [xml_of_type T])
+  | xml_of_term (Const (s, T)) =
+      XML.Elem (("Const", [("name", s)]), [xml_of_type T])
+  | xml_of_term (t $ u) =
+      XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
+  | xml_of_term (Abs (s, T, t)) =
+      XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
+
+fun xml_of_opttypes NONE = []
+  | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
+
+(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
+(* it can be looked up in the theorem database. Thus, it could be      *)
+(* omitted from the xml representation.                                *)
+
+(* FIXME not exhaustive *)
+fun xml_of_proof (PBound i) =
+      XML.Elem (("PBound", [("index", string_of_int i)]), [])
+  | xml_of_proof (Abst (s, optT, prf)) =
+      XML.Elem (("Abst", [("vname", s)]),
+        (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
+  | xml_of_proof (AbsP (s, optt, prf)) =
+      XML.Elem (("AbsP", [("vname", s)]),
+        (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
+  | xml_of_proof (prf % optt) =
+      XML.Elem (("Appt", []),
+        xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
+  | xml_of_proof (prf %% prf') =
+      XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
+  | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
+  | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
+      XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
+  | xml_of_proof (PAxm (s, t, optTs)) =
+      XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
+  | xml_of_proof (Oracle (s, t, optTs)) =
+      XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
+  | xml_of_proof MinProof =
+      XML.Elem (("MinProof", []), []);
+
+
+(* useful for checking the output against a schema file *)
+
+fun write_to_file path elname x =
+  File.write path
+    ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
+     XML.string_of (XML.Elem ((elname,
+         [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
+          ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
+       [x])));
+
+
+
+(**** XML input ****)
+
+exception XML of string * XML.tree;
+
+fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
+  | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
+
+fun index_of_string s tree idx =
+  (case Int.fromString idx of
+    NONE => raise XML (s ^ ": bad index", tree)
+  | SOME i => i);
+
+fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
+      ((case Properties.get atts "name" of
+          NONE => raise XML ("type_of_xml: name of TVar missing", tree)
+        | SOME name => name,
+        the_default 0 (Option.map (index_of_string "type_of_xml" tree)
+          (Properties.get atts "index"))),
+       map class_of_xml classes)
+  | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
+      TFree (s, map class_of_xml classes)
+  | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
+      Type (s, map type_of_xml types)
+  | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
+
+fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
+      Bound (index_of_string "bad variable index" tree idx)
+  | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
+      Free (s, type_of_xml typ)
+  | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
+      ((case Properties.get atts "name" of
+          NONE => raise XML ("type_of_xml: name of Var missing", tree)
+        | SOME name => name,
+        the_default 0 (Option.map (index_of_string "term_of_xml" tree)
+          (Properties.get atts "index"))),
+       type_of_xml typ)
+  | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
+      Const (s, type_of_xml typ)
+  | term_of_xml (XML.Elem (("App", []), [term, term'])) =
+      term_of_xml term $ term_of_xml term'
+  | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
+      Abs (s, type_of_xml typ, term_of_xml term)
+  | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
+
+fun opttypes_of_xml [] = NONE
+  | opttypes_of_xml [XML.Elem (("types", []), types)] =
+      SOME (map type_of_xml types)
+  | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
+
+fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
+      PBound (index_of_string "proof_of_xml" tree idx)
+  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
+      Abst (s, NONE, proof_of_xml proof)
+  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
+      Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
+  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
+      AbsP (s, NONE, proof_of_xml proof)
+  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
+      AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
+  | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
+      proof_of_xml proof % NONE
+  | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
+      proof_of_xml proof % SOME (term_of_xml term)
+  | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
+      proof_of_xml proof %% proof_of_xml proof'
+  | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
+      Hyp (term_of_xml term)
+  | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
+      (* FIXME? *)
+      PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
+        Future.value (Proofterm.approximate_proof_body MinProof)))
+  | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
+      PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
+  | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
+      Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
+  | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
+  | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
+
+end;
diff -r de77cde57376 -r ce1f0602f48e src/Pure/Tools/xml_syntax.ML
--- a/src/Pure/Tools/xml_syntax.ML	Mon Nov 26 16:22:29 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-(*  Title:      Pure/Tools/xml_syntax.ML
-    Author:     Stefan Berghofer, TU Muenchen
-
-Input and output of types, terms, and proofs in XML format.
-See isabelle.xsd for a description of the syntax.
-*)
-
-signature XML_SYNTAX =
-sig
-  val xml_of_type: typ -> XML.tree
-  val xml_of_term: term -> XML.tree
-  val xml_of_proof: Proofterm.proof -> XML.tree
-  val write_to_file: Path.T -> string -> XML.tree -> unit
-  exception XML of string * XML.tree
-  val type_of_xml: XML.tree -> typ
-  val term_of_xml: XML.tree -> term
-  val proof_of_xml: XML.tree -> Proofterm.proof
-end;
-
-structure XML_Syntax : XML_SYNTAX =
-struct
-
-(**** XML output ****)
-
-fun xml_of_class name = XML.Elem (("class", [("name", name)]), []);
-
-fun xml_of_type (TVar ((s, i), S)) =
-      XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
-        map xml_of_class S)
-  | xml_of_type (TFree (s, S)) =
-      XML.Elem (("TFree", [("name", s)]), map xml_of_class S)
-  | xml_of_type (Type (s, Ts)) =
-      XML.Elem (("Type", [("name", s)]), map xml_of_type Ts);
-
-fun xml_of_term (Bound i) =
-      XML.Elem (("Bound", [("index", string_of_int i)]), [])
-  | xml_of_term (Free (s, T)) =
-      XML.Elem (("Free", [("name", s)]), [xml_of_type T])
-  | xml_of_term (Var ((s, i), T)) =
-      XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])),
-        [xml_of_type T])
-  | xml_of_term (Const (s, T)) =
-      XML.Elem (("Const", [("name", s)]), [xml_of_type T])
-  | xml_of_term (t $ u) =
-      XML.Elem (("App", []), [xml_of_term t, xml_of_term u])
-  | xml_of_term (Abs (s, T, t)) =
-      XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]);
-
-fun xml_of_opttypes NONE = []
-  | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)];
-
-(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
-(* it can be looked up in the theorem database. Thus, it could be      *)
-(* omitted from the xml representation.                                *)
-
-(* FIXME not exhaustive *)
-fun xml_of_proof (PBound i) =
-      XML.Elem (("PBound", [("index", string_of_int i)]), [])
-  | xml_of_proof (Abst (s, optT, prf)) =
-      XML.Elem (("Abst", [("vname", s)]),
-        (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf])
-  | xml_of_proof (AbsP (s, optt, prf)) =
-      XML.Elem (("AbsP", [("vname", s)]),
-        (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf])
-  | xml_of_proof (prf % optt) =
-      XML.Elem (("Appt", []),
-        xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t]))
-  | xml_of_proof (prf %% prf') =
-      XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf'])
-  | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t])
-  | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
-      XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
-  | xml_of_proof (PAxm (s, t, optTs)) =
-      XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
-  | xml_of_proof (Oracle (s, t, optTs)) =
-      XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs)
-  | xml_of_proof MinProof =
-      XML.Elem (("MinProof", []), []);
-
-
-(* useful for checking the output against a schema file *)
-
-fun write_to_file path elname x =
-  File.write path
-    ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
-     XML.string_of (XML.Elem ((elname,
-         [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
-          ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]),
-       [x])));
-
-
-
-(**** XML input ****)
-
-exception XML of string * XML.tree;
-
-fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name
-  | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree);
-
-fun index_of_string s tree idx =
-  (case Int.fromString idx of
-    NONE => raise XML (s ^ ": bad index", tree)
-  | SOME i => i);
-
-fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar
-      ((case Properties.get atts "name" of
-          NONE => raise XML ("type_of_xml: name of TVar missing", tree)
-        | SOME name => name,
-        the_default 0 (Option.map (index_of_string "type_of_xml" tree)
-          (Properties.get atts "index"))),
-       map class_of_xml classes)
-  | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) =
-      TFree (s, map class_of_xml classes)
-  | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) =
-      Type (s, map type_of_xml types)
-  | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree);
-
-fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) =
-      Bound (index_of_string "bad variable index" tree idx)
-  | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) =
-      Free (s, type_of_xml typ)
-  | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var
-      ((case Properties.get atts "name" of
-          NONE => raise XML ("type_of_xml: name of Var missing", tree)
-        | SOME name => name,
-        the_default 0 (Option.map (index_of_string "term_of_xml" tree)
-          (Properties.get atts "index"))),
-       type_of_xml typ)
-  | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) =
-      Const (s, type_of_xml typ)
-  | term_of_xml (XML.Elem (("App", []), [term, term'])) =
-      term_of_xml term $ term_of_xml term'
-  | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) =
-      Abs (s, type_of_xml typ, term_of_xml term)
-  | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree);
-
-fun opttypes_of_xml [] = NONE
-  | opttypes_of_xml [XML.Elem (("types", []), types)] =
-      SOME (map type_of_xml types)
-  | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree);
-
-fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) =
-      PBound (index_of_string "proof_of_xml" tree idx)
-  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) =
-      Abst (s, NONE, proof_of_xml proof)
-  | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) =
-      Abst (s, SOME (type_of_xml typ), proof_of_xml proof)
-  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) =
-      AbsP (s, NONE, proof_of_xml proof)
-  | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) =
-      AbsP (s, SOME (term_of_xml term), proof_of_xml proof)
-  | proof_of_xml (XML.Elem (("Appt", []), [proof])) =
-      proof_of_xml proof % NONE
-  | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) =
-      proof_of_xml proof % SOME (term_of_xml term)
-  | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) =
-      proof_of_xml proof %% proof_of_xml proof'
-  | proof_of_xml (XML.Elem (("Hyp", []), [term])) =
-      Hyp (term_of_xml term)
-  | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) =
-      (* FIXME? *)
-      PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
-        Future.value (Proofterm.approximate_proof_body MinProof)))
-  | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) =
-      PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
-  | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) =
-      Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
-  | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof
-  | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
-
-end;