# HG changeset patch
# User wenzelm
# Date 850726937 -3600
# Node ID edcc26b1461dfb00ce60d90086aed5f9d396062e
# Parent  8115988ccc22745eb7039ae13444d3a972db8755
added symbol_input.ML;

diff -r 8115988ccc22 -r edcc26b1461d src/Pure/Thy/ROOT.ML
--- 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 () =