Added clause for hypotheses to proof_of_xml function.
authorberghofe
Tue, 17 Jul 2007 16:05:34 +0200
changeset 2383164e6e5c738a1
parent 23830 f838adde842d
child 23832 09ee9527ffce
Added clause for hypotheses to proof_of_xml function.
src/Pure/Tools/xml_syntax.ML
     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)