# HG changeset patch
# User wenzelm
# Date 933883763 -7200
# Node ID 6bb7ad30f3da93300b0ebd32eae1f7047574f5c7
# Parent  a329a37ed91aef4e97e2f78bf4c1f18b18ab68ca
change_simpset_of;

diff -r a329a37ed91a -r 6bb7ad30f3da src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Thu Aug 05 22:08:53 1999 +0200
+++ b/src/Provers/simplifier.ML	Thu Aug 05 22:09:23 1999 +0200
@@ -91,6 +91,7 @@
   val simp_add_local: Proof.context attribute
   val simp_del_local: Proof.context attribute
   val simp_only_local: Proof.context attribute
+  val change_simpset_of: (simpset * 'a -> simpset) -> 'a -> theory -> theory
   val simp_modifiers: (Args.T list -> (Proof.context attribute * Args.T list)) list
   val setup: (theory -> theory) list
 end;
@@ -293,7 +294,11 @@
 
 (* change global simpset *)
 
-fun change_simpset f x = simpset_ref () := (f (simpset (), x));
+fun change_simpset_of f x thy =
+  let val r = simpset_ref_of thy
+  in r := f (! r, x); thy end;
+
+fun change_simpset f x = (change_simpset_of f x (Context.the_context ()); ());
 
 val Addsimps = change_simpset (op addsimps);
 val Delsimps = change_simpset (op delsimps);