1.1 --- a/src/HOL/Import/xmlconv.ML	Sat Nov 15 21:31:36 2008 +0100
     1.2 +++ b/src/HOL/Import/xmlconv.ML	Sat Nov 15 21:31:37 2008 +0100
     1.3 @@ -143,13 +143,13 @@
     1.4    | xml_of_proof (prf %% prf') =
     1.5        XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
     1.6    | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
     1.7 -  | xml_of_proof (PThm (s, _, t, optTs)) =
     1.8 +  | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
     1.9        XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
    1.10    | xml_of_proof (PAxm (s, t, optTs)) =
    1.11        XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
    1.12    | xml_of_proof (Oracle (s, t, optTs)) =
    1.13        XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
    1.14 -  | xml_of_proof (MinProof _) = XML.Elem ("MinProof", [], []);
    1.15 +  | xml_of_proof MinProof = XML.Elem ("MinProof", [], []);
    1.16  
    1.17  fun xml_of_bool b = XML.Elem ("bool", [("value", if b then "true" else "false")], [])
    1.18  fun xml_of_int i = XML.Elem ("int", [("value", string_of_int i)], [])

     2.1 --- a/src/Pure/Tools/xml_syntax.ML	Sat Nov 15 21:31:36 2008 +0100
     2.2 +++ b/src/Pure/Tools/xml_syntax.ML	Sat Nov 15 21:31:37 2008 +0100
     2.3 @@ -71,13 +71,13 @@
     2.4    | xml_of_proof (prf %% prf') =
     2.5        XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
     2.6    | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
     2.7 -  | xml_of_proof (PThm (s, _, t, optTs)) =
     2.8 +  | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
     2.9        XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
    2.10    | xml_of_proof (PAxm (s, t, optTs)) =
    2.11        XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
    2.12    | xml_of_proof (Oracle (s, t, optTs)) =
    2.13        XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
    2.14 -  | xml_of_proof (MinProof prfs) =
    2.15 +  | xml_of_proof MinProof =
    2.16        XML.Elem ("MinProof", [], []);
    2.17  
    2.18  (* useful for checking the output against a schema file *)
    2.19 @@ -157,13 +157,14 @@
    2.20    | proof_of_xml (XML.Elem ("Hyp", [], [term])) =
    2.21        Hyp (term_of_xml term)
    2.22    | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
    2.23 -      PThm (s, MinProof ([], [], []),  (* FIXME? *)
    2.24 -        term_of_xml term, opttypes_of_xml opttypes)
    2.25 +      (* FIXME? *)
    2.26 +      PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
    2.27 +        Lazy.value (Proofterm.make_proof_body MinProof)))
    2.28    | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
    2.29        PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
    2.30    | proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =
    2.31        Oracle (s, term_of_xml term, opttypes_of_xml opttypes)
    2.32 -  | proof_of_xml (XML.Elem ("MinProof", _, _)) = MinProof ([], [], [])
    2.33 +  | proof_of_xml (XML.Elem ("MinProof", _, _)) = MinProof
    2.34    | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree);
    2.35  
    2.36  end;