diff -r f838adde842d -r 64e6e5c738a1 src/Pure/Tools/xml_syntax.ML --- a/src/Pure/Tools/xml_syntax.ML Tue Jul 17 15:59:50 2007 +0200 +++ b/src/Pure/Tools/xml_syntax.ML Tue Jul 17 16:05:34 2007 +0200 @@ -154,6 +154,8 @@ 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)) = PThm (s, MinProof ([], [], []), (* FIXME? *) term_of_xml term, opttypes_of_xml opttypes)