diff -r 6bbb42843b6e -r ada3ab6b9085 src/Pure/ProofGeneral/pgip_markup.ML
--- a/src/Pure/ProofGeneral/pgip_markup.ML	Sat Aug 07 19:52:14 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_markup.ML	Sat Aug 07 21:03:06 2010 +0200
@@ -75,81 +75,81 @@
        case docelt of
 
            Openblock vs  =>
-           XML.Elem("openblock", opt_attr "name" (#metavarid vs) @
-                                 opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
-                                 opt_attr "metavarid" (#metavarid vs),
+           XML.Elem(("openblock", opt_attr "name" (#metavarid vs) @
+                                  opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
+                                  opt_attr "metavarid" (#metavarid vs)),
                     [])
 
          | Closeblock _ =>
-           XML.Elem("closeblock", [], [])
+           XML.Elem(("closeblock", []), [])
 
          | Opentheory vs  =>
-           XML.Elem("opentheory",
+           XML.Elem(("opentheory",
                     opt_attr "thyname" (#thyname vs) @
                     opt_attr "parentnames"
                              (case (#parentnames vs)
                                of [] => NONE
-                                | ps => SOME (space_implode ";" ps)),
+                                | ps => SOME (space_implode ";" ps))),
                     [XML.Text (#text vs)])
 
          | Theoryitem vs =>
-           XML.Elem("theoryitem",
+           XML.Elem(("theoryitem",
                     opt_attr "name" (#name vs) @
-                    opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs),
+                    opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs)),
                     [XML.Text (#text vs)])
 
          | Closetheory vs =>
-           XML.Elem("closetheory", [], [XML.Text (#text vs)])
+           XML.Elem(("closetheory", []), [XML.Text (#text vs)])
 
          | Opengoal vs =>
-           XML.Elem("opengoal",
-                    opt_attr "thmname" (#thmname vs),
+           XML.Elem(("opengoal",
+                    opt_attr "thmname" (#thmname vs)),
                     [XML.Text (#text vs)])
 
          | Proofstep vs =>
-           XML.Elem("proofstep", [], [XML.Text (#text vs)])
+           XML.Elem(("proofstep", []), [XML.Text (#text vs)])
 
          | Closegoal vs =>
-           XML.Elem("closegoal", [], [XML.Text (#text vs)])
+           XML.Elem(("closegoal", []), [XML.Text (#text vs)])
 
          | Giveupgoal vs =>
-           XML.Elem("giveupgoal", [], [XML.Text (#text vs)])
+           XML.Elem(("giveupgoal", []), [XML.Text (#text vs)])
 
          | Postponegoal vs =>
-           XML.Elem("postponegoal", [], [XML.Text (#text vs)])
+           XML.Elem(("postponegoal", []), [XML.Text (#text vs)])
 
          | Comment vs =>
-           XML.Elem("comment", [], [XML.Text (#text vs)])
+           XML.Elem(("comment", []), [XML.Text (#text vs)])
 
          | Whitespace vs =>
-           XML.Elem("whitespace", [], [XML.Text (#text vs)])
+           XML.Elem(("whitespace", []), [XML.Text (#text vs)])
 
          | Doccomment vs =>
-           XML.Elem("doccomment", [], [XML.Text (#text vs)])
+           XML.Elem(("doccomment", []), [XML.Text (#text vs)])
 
          | Spuriouscmd vs =>
-           XML.Elem("spuriouscmd", [], [XML.Text (#text vs)])
+           XML.Elem(("spuriouscmd", []), [XML.Text (#text vs)])
 
          | Badcmd vs =>
-           XML.Elem("badcmd", [], [XML.Text (#text vs)])
+           XML.Elem(("badcmd", []), [XML.Text (#text vs)])
 
          | Unparseable vs =>
-           XML.Elem("unparseable", [], [XML.Text (#text vs)])
+           XML.Elem(("unparseable", []), [XML.Text (#text vs)])
 
          | Metainfo vs =>
-           XML.Elem("metainfo", opt_attr "name" (#name vs),
+           XML.Elem(("metainfo", opt_attr "name" (#name vs)),
                     [XML.Text (#text vs)])
 
          | Litcomment vs =>
-           XML.Elem("litcomment", opt_attr "format" (#format vs),
+           XML.Elem(("litcomment", opt_attr "format" (#format vs)),
                    #content vs)
 
          | Showcode vs =>
-           XML.Elem("showcode",
-                    attr "show" (PgipTypes.bool_to_pgstring (#show vs)), [])
+           XML.Elem(("showcode",
+                    attr "show" (PgipTypes.bool_to_pgstring (#show vs))), [])
 
          | Setformat vs =>
-           XML.Elem("setformat", attr "format" (#format vs), [])
+           XML.Elem(("setformat", attr "format" (#format vs)), [])
 
    val output_doc = map xml_of