src/Sequents/simpdata.ML

--- a/src/Sequents/simpdata.ML	Mon Oct 17 23:10:10 2005 +0200
+++ b/src/Sequents/simpdata.ML	Mon Oct 17 23:10:13 2005 +0200
@@ -223,8 +223,6 @@
 qed "if_not_P";
 
 
-open Simplifier;
-
 (*** Standard simpsets ***)
 
 val triv_rls = [FalseL, TrueR, basic, refl, iff_refl, reflexive_thm];
@@ -259,7 +257,7 @@
   addeqcongs [left_cong]
   addcongs [imp_cong];
 
-simpset_ref() := LK_ss;
+change_simpset (fn _ => LK_ss);
 
 
 (* To create substition rules *)