XML.string_of;
authorwenzelm
Thu, 03 Apr 2008 18:42:42 +0200
changeset 26544 af4c77a21c06
parent 26543 cd01c8eb314a
child 26545 6e1aef001b3b
XML.string_of;
src/Pure/Tools/xml_syntax.ML
--- a/src/Pure/Tools/xml_syntax.ML	Thu Apr 03 18:42:41 2008 +0200
+++ b/src/Pure/Tools/xml_syntax.ML	Thu Apr 03 18:42:42 2008 +0200
@@ -85,7 +85,7 @@
 fun write_to_file path elname x =
   File.write path
     ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n" ^
-     XML.string_of_tree (XML.Elem (elname,
+     XML.string_of (XML.Elem (elname,
        [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"),
         ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")],
        [x])));