src/Pure/General/ROOT.ML
changeset 30587 ad19c99529eb
parent 30360 d4d3fafc9bca
child 31326 deddd77112b7
--- a/src/Pure/General/ROOT.ML	Thu Mar 19 15:22:53 2009 +0100
+++ b/src/Pure/General/ROOT.ML	Thu Mar 19 15:22:53 2009 +0100
@@ -15,6 +15,7 @@
 use "seq.ML";
 use "position.ML";
 use "symbol_pos.ML";
+use "antiquote.ML";
 use "../ML/ml_lex.ML";
 use "../ML/ml_parse.ML";
 use "secure.ML";