# HG changeset patch
# User aspinall
# Date 1126793722 -7200
# Node ID 38e0219ec0225bcd5e273b125fd75ca246c9504f
# Parent  3813cc8fad5550c8dd548ed3e76c2a89282e0311
Revert previous attribute name change, problem can be avoided in JAXB.

diff -r 3813cc8fad55 -r 38e0219ec022 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Thu Sep 15 13:36:10 2005 +0200
+++ b/src/Pure/proof_general.ML	Thu Sep 15 16:15:22 2005 +0200
@@ -180,7 +180,7 @@
     XML.element
       "pgip"
       ([("tag",    pgip_tag),
-        ("messageclass",  pgip_class),
+        ("class",  pgip_class),
         ("seq",    string_of_int (pgip_serial())),
         ("id",     !pgip_id)] @
        if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
@@ -1298,7 +1298,7 @@
      (case xml of
           XML.Elem ("pgip", attrs, pgips) =>
           (let
-               val class = xmlattr "messageclass" attrs
+               val class = xmlattr "class" attrs
                val dest  = xmlattro "destid" attrs
                val _ = (pgip_refid :=  xmlattro "id" attrs;
                         pgip_refseq := xmlattro "seq" attrs)