added symbol_input.ML;
authorwenzelm
Mon Dec 16 10:02:17 1996 +0100 (1996-12-16)
changeset 2404edcc26b1461d
parent 2403 8115988ccc22
child 2405 e1b946f9c8be
added symbol_input.ML;
src/Pure/Thy/ROOT.ML
     1.1 --- a/src/Pure/Thy/ROOT.ML	Mon Dec 16 10:01:40 1996 +0100
     1.2 +++ b/src/Pure/Thy/ROOT.ML	Mon Dec 16 10:02:17 1996 +0100
     1.3 @@ -11,13 +11,13 @@
     1.4  use "thy_syn.ML";
     1.5  use "thm_database.ML";
     1.6  use "../../Provers/simplifier.ML";
     1.7 -
     1.8 +use "symbol_input.ML";
     1.9  use "thy_read.ML";
    1.10  
    1.11  structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
    1.12  structure ThmDB = ThmDBFun();
    1.13  structure ReadThy = ReadthyFun(structure ThySyn = ThySyn and ThmDB = ThmDB);
    1.14 -open ThmDB ReadThy;
    1.15 +open ThmDB ReadThy SymbolInput;
    1.16  
    1.17  
    1.18  fun init_thy_reader () =