src/Pure/ROOT.ML
changeset 59064 a8bcb5a446c8
parent 59054 61b723761dff
child 59086 94b2690ad494
--- a/src/Pure/ROOT.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/ROOT.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -32,6 +32,7 @@
 use "General/symbol.ML";
 use "General/position.ML";
 use "General/symbol_pos.ML";
+use "General/input.ML";
 use "General/antiquote.ML";
 use "ML/ml_lex.ML";
 use "ML/ml_parse.ML";