diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/ROOT.ML
--- 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";