remove references to simplifier.ML;
authorwenzelm
Fri, 25 Jul 1997 13:17:14 +0200
changeset 3576 9cd0a0919ba0
parent 3575 4e9beacb5339
child 3577 9715b6e3ec5f
remove references to simplifier.ML;
src/Pure/Thy/ROOT.ML
src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/ROOT.ML	Fri Jul 25 11:47:09 1997 +0200
+++ b/src/Pure/Thy/ROOT.ML	Fri Jul 25 13:17:14 1997 +0200
@@ -10,7 +10,6 @@
 use "thy_parse.ML";
 use "thy_syn.ML";
 use "thm_database.ML";
-use "../../Provers/simplifier.ML";
 use "symbol_input.ML";
 use "thy_read.ML";
 
--- a/src/Pure/Thy/thy_read.ML	Fri Jul 25 11:47:09 1997 +0200
+++ b/src/Pure/Thy/thy_read.ML	Fri Jul 25 13:17:14 1997 +0200
@@ -5,7 +5,7 @@
     Copyright   1994 TU Muenchen
 
 Functions for reading theory files, and storing and retrieving theories,
-theorems and the global simplifier set.
+theorems.
 *)
 
 (*Types for theory storage*)
@@ -111,7 +111,7 @@
 functor ReadthyFun(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY =
 struct
 
-open ThmDB Simplifier;
+open ThmDB;
 
 datatype basetype = Thy  of string
                   | File of string;