# HG changeset patch
# User wenzelm
# Date 869829434 -7200
# Node ID 9cd0a0919ba07a76f99cde841d202bbc26304fc1
# Parent  4e9beacb53397833eb606dca452b85b19fab1831
remove references to simplifier.ML;

diff -r 4e9beacb5339 -r 9cd0a0919ba0 src/Pure/Thy/ROOT.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";
 
diff -r 4e9beacb5339 -r 9cd0a0919ba0 src/Pure/Thy/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;