remove references to simplifier.ML;
authorwenzelm
Fri Jul 25 13:17:14 1997 +0200 (1997-07-25)
changeset 35769cd0a0919ba0
parent 3575 4e9beacb5339
child 3577 9715b6e3ec5f
remove references to simplifier.ML;
src/Pure/Thy/ROOT.ML
src/Pure/Thy/thy_read.ML
     1.1 --- a/src/Pure/Thy/ROOT.ML	Fri Jul 25 11:47:09 1997 +0200
     1.2 +++ b/src/Pure/Thy/ROOT.ML	Fri Jul 25 13:17:14 1997 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4  use "thy_parse.ML";
     1.5  use "thy_syn.ML";
     1.6  use "thm_database.ML";
     1.7 -use "../../Provers/simplifier.ML";
     1.8  use "symbol_input.ML";
     1.9  use "thy_read.ML";
    1.10  
     2.1 --- a/src/Pure/Thy/thy_read.ML	Fri Jul 25 11:47:09 1997 +0200
     2.2 +++ b/src/Pure/Thy/thy_read.ML	Fri Jul 25 13:17:14 1997 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4      Copyright   1994 TU Muenchen
     2.5  
     2.6  Functions for reading theory files, and storing and retrieving theories,
     2.7 -theorems and the global simplifier set.
     2.8 +theorems.
     2.9  *)
    2.10  
    2.11  (*Types for theory storage*)
    2.12 @@ -111,7 +111,7 @@
    2.13  functor ReadthyFun(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY =
    2.14  struct
    2.15  
    2.16 -open ThmDB Simplifier;
    2.17 +open ThmDB;
    2.18  
    2.19  datatype basetype = Thy  of string
    2.20                    | File of string;