# HG changeset patch
# User aspinall
# Date 1183658341 -7200
# Node ID aaba731fce8655c2c898e8ea0fc290a77020b3a3
# Parent  4fc6df2c709868ad11fa6b5d980384542fc06ce9
Revert body of pgml to match schema for now [change bad for Broker]

diff -r 4fc6df2c7098 -r aaba731fce86 src/Pure/ProofGeneral/pgml.ML
--- a/src/Pure/ProofGeneral/pgml.ML	Thu Jul 05 19:57:19 2007 +0200
+++ b/src/Pure/ProofGeneral/pgml.ML	Thu Jul 05 19:59:01 2007 +0200
@@ -37,7 +37,7 @@
 
     datatype pgmldoc =
 	     Pgml of { version: string option, systemid: string option, 
-		       content: pgmlterm list }
+		       content: pgmlterm }
 
     val pgmlterm_to_xml : pgmlterm -> XML.tree
 
@@ -78,7 +78,7 @@
 
     datatype pgmldoc =
 	     Pgml of { version: string option, systemid: string option, 
-		       content: pgmlterm list }
+		       content: pgmlterm }
 
     fun pgmlorient_to_string HOVOrient = "hov"
       | pgmlorient_to_string HOrient = "h"
@@ -138,5 +138,5 @@
 
     fun pgmldoc_to_xml (Pgml {version,systemid,content}) = 
 	XML.Elem("pgml",opt_attr "version" version  @ opt_attr "systemid" systemid,
-		 map pgmlterm_to_xml content)
+		 [pgmlterm_to_xml content])
 end