# HG changeset patch
# User berghofe
# Date 1184681134 -7200
# Node ID 64e6e5c738a10e600403cbf2156f4b0869d46aa3
# Parent  f838adde842d697f2d940a9ecadf21b8c8e88e79
Added clause for hypotheses to proof_of_xml function.

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)