Added clause for hypotheses to proof_of_xml function.
1.1 --- a/src/Pure/Tools/xml_syntax.ML Tue Jul 17 15:59:50 2007 +0200
1.2 +++ b/src/Pure/Tools/xml_syntax.ML Tue Jul 17 16:05:34 2007 +0200
1.3 @@ -154,6 +154,8 @@
1.4 proof_of_xml proof % SOME (term_of_xml term)
1.5 | proof_of_xml (XML.Elem ("AppP", [], [proof, proof'])) =
1.6 proof_of_xml proof %% proof_of_xml proof'
1.7 + | proof_of_xml (XML.Elem ("Hyp", [], [term])) =
1.8 + Hyp (term_of_xml term)
1.9 | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
1.10 PThm (s, MinProof ([], [], []), (* FIXME? *)
1.11 term_of_xml term, opttypes_of_xml opttypes)