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