# HG changeset patch
# User berghofe
# Date 1158846049 -7200
# Node ID da6e410c5387c682953ba6ed79458e7fc3077a2a
# Parent  9de0a076b3fc156907c11bb78b81e8ece2f58eee
Added xml_syntax.ML

diff -r 9de0a076b3fc -r da6e410c5387 src/Pure/Tools/ROOT.ML
--- a/src/Pure/Tools/ROOT.ML	Thu Sep 21 15:40:31 2006 +0200
+++ b/src/Pure/Tools/ROOT.ML	Thu Sep 21 15:40:49 2006 +0200
@@ -31,3 +31,6 @@
 use "nbe_eval.ML";
 use "nbe_codegen.ML";
 use "nbe.ML";
+
+(*XML syntax for terms and types*)
+use "xml_syntax.ML";