src/Pure/ROOT.ML
changeset 52926 6415d95bf7a2
parent 52865 02a7e7180ee5
child 53192 04df1d236e1c
--- a/src/Pure/ROOT.ML	Thu Aug 08 23:34:52 2013 +0200
+++ b/src/Pure/ROOT.ML	Thu Aug 08 23:52:35 2013 +0200
@@ -302,7 +302,6 @@
 use "Tools/build.ML";
 use "Tools/named_thms.ML";
 use "Tools/proof_general.ML";
-use "Tools/legacy_xml_syntax.ML";
 
 
 (* ML toplevel pretty printing *)