# HG changeset patch
# User wenzelm
# Date 954532714 -7200
# Node ID 31bcb6b64d60c215fe7ac256d179a41914c5ff93
# Parent  21cb46716f32e214494a6253a421edd31ed615ca
added change_global/local_css;

diff -r 21cb46716f32 -r 31bcb6b64d60 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Fri Mar 31 21:57:14 2000 +0200
+++ b/src/Provers/clasimp.ML	Fri Mar 31 21:58:34 2000 +0200
@@ -45,6 +45,8 @@
   val force_tac	  : clasimpset  -> int -> tactic
   val Force_tac	  : int -> tactic
   val force	  : int -> unit
+  val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
+  val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
   val setup	  : (theory -> theory) list
 end;
 
@@ -148,6 +150,27 @@
 fun force i = by (Force_tac i);
 
 
+(* attributes *)
+
+fun change_global_css f (thy, th) =
+  let
+    val cs_ref = Classical.claset_ref_of thy;
+    val ss_ref = Simplifier.simpset_ref_of thy;
+    val (cs', ss') = f ((! cs_ref, ! ss_ref), [th]);
+  in cs_ref := cs'; ss_ref := ss'; (thy, th) end;
+
+fun change_local_css f (ctxt, th) =
+  let
+    val cs = Classical.get_local_claset ctxt;
+    val ss = Simplifier.get_local_simpset ctxt;
+    val (cs', ss') = f ((cs, ss), [th]);
+    val ctxt' =
+      ctxt
+      |> Classical.put_local_claset cs'
+      |> Simplifier.put_local_simpset ss';
+  in (ctxt', th) end;
+
+
 (* methods *)
 
 fun get_local_clasimpset ctxt =