src/Pure/Thy/ROOT.ML
changeset 1242 b3f68a644380
parent 1221 19dde7bfcd07
child 1261 af4107a03150
     1.1 --- a/src/Pure/Thy/ROOT.ML	Fri Sep 01 13:27:48 1995 +0200
     1.2 +++ b/src/Pure/Thy/ROOT.ML	Fri Sep 01 13:28:54 1995 +0200
     1.3 @@ -15,11 +15,14 @@
     1.4  
     1.5  use "thy_syn.ML";
     1.6  use "thm_database.ML";
     1.7 +use "../../Provers/simplifier.ML";
     1.8  use "thy_read.ML";
     1.9  
    1.10  structure ThySyn = ThySynFun(val user_keywords = [] and user_sections = []);
    1.11 -structure ThmDB = ThmDBFun();
    1.12 -structure Readthy = ReadthyFUN(structure ThySyn = ThySyn and ThmDB = ThmDB);
    1.13 +structure ThmDB = ThmDBFUN();
    1.14 +structure Simplifier = SimplifierFUN();
    1.15 +structure Readthy = ReadthyFUN(structure ThySyn = ThySyn and ThmDB = ThmDB
    1.16 +                               and Simplifier = Simplifier);
    1.17  open ThmDB Readthy;
    1.18  
    1.19  (* hide functors; saves space in PolyML *)
    1.20 @@ -28,9 +31,11 @@
    1.21  
    1.22  fun init_thy_reader () =
    1.23    use_string
    1.24 -   ["structure ThmDB = ThmDBFun();",
    1.25 +   ["structure ThmDB = ThmDBFUN();",
    1.26 +    "structure Simplifier = SimplifierFUN();",
    1.27      "structure Readthy = ReadthyFUN(structure ThySyn = ThySyn \
    1.28 -                                   \and ThmDB = ThmDB);",
    1.29 +                                   \and ThmDB = ThmDB \
    1.30 +                                   \and Simplifier = Simplifier);",
    1.31      "Readthy.loaded_thys := !loaded_thys;",
    1.32      "ThmDB.thm_db := !thm_db;",
    1.33      "val first_init_readthy = false;",