# HG changeset patch
# User wenzelm
# Date 1226781097 -3600
# Node ID aa36d05926ec9223ca1a1442dfe9524f0ba5802c
# Parent  e915ab11fe52fc0e885c3bb71368fc95e8bf6edd
adapted PThm and MinProof;

diff -r e915ab11fe52 -r aa36d05926ec src/HOL/Import/xmlconv.ML
--- a/src/HOL/Import/xmlconv.ML	Sat Nov 15 21:31:36 2008 +0100
+++ b/src/HOL/Import/xmlconv.ML	Sat Nov 15 21:31:37 2008 +0100
@@ -143,13 +143,13 @@
   | 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_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", [], []);
+  | xml_of_proof MinProof = XML.Elem ("MinProof", [], []);
 
 fun xml_of_bool b = XML.Elem ("bool", [("value", if b then "true" else "false")], [])
 fun xml_of_int i = XML.Elem ("int", [("value", string_of_int i)], [])
diff -r e915ab11fe52 -r aa36d05926ec src/Pure/Tools/xml_syntax.ML
--- a/src/Pure/Tools/xml_syntax.ML	Sat Nov 15 21:31:36 2008 +0100
+++ b/src/Pure/Tools/xml_syntax.ML	Sat Nov 15 21:31:37 2008 +0100
@@ -71,13 +71,13 @@
   | 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_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 prfs) =
+  | xml_of_proof MinProof =
       XML.Elem ("MinProof", [], []);
 
 (* useful for checking the output against a schema file *)
@@ -157,13 +157,14 @@
   | proof_of_xml (XML.Elem ("Hyp", [], [term])) =
       Hyp (term_of_xml term)
   | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
-      PThm (s, MinProof ([], [], []),  (* FIXME? *)
-        term_of_xml term, opttypes_of_xml opttypes)
+      (* FIXME? *)
+      PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
+        Lazy.value (Proofterm.make_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 (XML.Elem ("MinProof", _, _)) = MinProof
   | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
 
 end;