--- a/src/Pure/Thy/ROOT.ML Mon Dec 16 10:01:40 1996 +0100
+++ b/src/Pure/Thy/ROOT.ML Mon Dec 16 10:02:17 1996 +0100
@@ -11,13 +11,13 @@
use "thy_syn.ML";
use "thm_database.ML";
use "../../Provers/simplifier.ML";
-
+use "symbol_input.ML";
use "thy_read.ML";
structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
structure ThmDB = ThmDBFun();
structure ReadThy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB);
-open ThmDB ReadThy;
+open ThmDB ReadThy SymbolInput;
fun init_thy_reader () =