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";