# HG changeset patch
# User wenzelm
# Date 1257192430 -3600
# Node ID 73c8987dc9f02d515eb1716f223266404f50e73b
# Parent  91b9da2a7b440830c88e4377ded96121e5495d75
modernized structure XML_Syntax;

diff -r 91b9da2a7b44 -r 73c8987dc9f0 src/Pure/Tools/xml_syntax.ML
--- a/src/Pure/Tools/xml_syntax.ML	Mon Nov 02 21:05:47 2009 +0100
+++ b/src/Pure/Tools/xml_syntax.ML	Mon Nov 02 21:07:10 2009 +0100
@@ -17,7 +17,7 @@
   val proof_of_xml: XML.tree -> Proofterm.proof
 end;
 
-structure XMLSyntax : XML_SYNTAX =
+structure XML_Syntax : XML_SYNTAX =
 struct
 
 (**** XML output ****)