diff -r b3f68a644380 -r fa09705a5890 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Fri Sep 01 13:28:54 1995 +0200
+++ b/src/Provers/simplifier.ML	Fri Sep 01 13:32:13 1995 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Provers/simplifier
+(*  Title:      Provers/simplifier.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1993  TU Munich
@@ -26,6 +26,13 @@
   val setmksimps: simpset * (thm -> thm list) -> simpset
   val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
   val simp_tac: simpset -> int -> tactic
+
+  val simpset: simpset ref
+  val Addsimps: thm list -> unit
+  val Delsimps: thm list -> unit
+  val Simp_tac: int -> tactic
+  val Asm_simp_tac: int -> tactic
+  val Asm_full_simp_tac: int -> tactic
 end;
 
 functor SimplifierFUN():SIMPLIFIER =
@@ -47,6 +54,7 @@
      finish_tac= K(K no_tac),
      loop_tac= K no_tac};
 
+val simpset = ref empty_ss;
 
 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,...}) setloop loop_tac =
   SS{mss=mss,
@@ -90,6 +98,8 @@
      loop_tac=loop_tac}
   end;
 
+fun Addsimps rews = (simpset := !simpset addsimps rews);
+
 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) delsimps rews =
   let val rews' = flat(map (Thm.mk_rews_of_mss mss) rews) in
   SS{mss= Thm.del_simps(mss,rews'),
@@ -100,6 +110,8 @@
      loop_tac=loop_tac}
   end;
 
+fun Delsimps rews = (simpset := !simpset delsimps rews);
+
 fun (SS{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) addeqcongs newcongs =
   SS{mss= Thm.add_congs(mss,newcongs),
      simps= simps,
@@ -156,6 +168,8 @@
 val asm_simp_tac = gen_simp_tac (false,true);
 val simp_tac = gen_simp_tac (false,false);
 
-end;
+fun Asm_full_simp_tac i = asm_full_simp_tac (!simpset) i;
+fun Asm_simp_tac i = asm_simp_tac (!simpset) i;
+fun Simp_tac i = simp_tac (!simpset) i;
 
-structure Simplifier = SimplifierFUN();
+end;