src/Pure/ProofGeneral/pgip_output.ML

--- a/src/Pure/ProofGeneral/pgip_output.ML	Fri Jul 06 17:21:18 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_output.ML	Fri Jul 06 17:52:52 2007 +0200
@@ -21,7 +21,7 @@
     | Informfileloaded    of { url: PgipTypes.pgipurl, completed: bool }
     | Informfileoutdated  of { url: PgipTypes.pgipurl, completed: bool }
     | Informfileretracted of { url: PgipTypes.pgipurl, completed: bool }
-    | Proofstate          of { pgml: XML.content }
+    | Proofstate          of { pgml: Pgml.pgmldoc }
     | Metainforesponse    of { attrs: XML.attributes, 
                                content: XML.content }
     | Lexicalstructure    of { content: XML.content }
@@ -81,7 +81,7 @@
        | Informfileloaded    of { url: Path.T, completed: bool }
        | Informfileoutdated  of { url: Path.T, completed: bool }
        | Informfileretracted of { url: Path.T, completed: bool }
-       | Proofstate          of { pgml: XML.content }
+       | Proofstate          of { pgml: Pgml.pgmldoc }
        | Metainforesponse    of { attrs: XML.attributes, content: XML.content }
        | Lexicalstructure    of { content: XML.content }
        | Proverinfo          of { name: string, version: string, instance: string,
@@ -194,7 +194,7 @@
     let
         val pgml = #pgml vs
     in
-        XML.Elem("proofstate", [], pgml)
+        XML.Elem("proofstate", [], [Pgml.pgmldoc_to_xml pgml])
     end
 
 fun metainforesponse (Metainforesponse vs) =