# 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 ****)