--- 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;