src/Pure/term_xml.ML
changeset 43779 47bec02c6762
parent 43778 ce9189450447
child 43789 321ebd051897
--- a/src/Pure/term_xml.ML	Tue Jul 12 17:53:06 2011 +0200
+++ b/src/Pure/term_xml.ML	Tue Jul 12 18:00:05 2011 +0200
@@ -14,15 +14,13 @@
 
 signature TERM_XML =
 sig
-  structure Encode: TERM_XML_OPS where type 'a T = 'a XML.Encode.T
-  structure Decode: TERM_XML_OPS where type 'a T = 'a XML.Decode.T
+  structure Encode: TERM_XML_OPS
+  structure Decode: TERM_XML_OPS
 end;
 
 structure Term_XML: TERM_XML =
 struct
 
-(* encode *)
-
 structure Encode =
 struct
 
@@ -45,9 +43,6 @@
 
 end;
 
-
-(* decode *)
-
 structure Decode =
 struct