export Simplifier.with_context;

--- a/src/Pure/simplifier.ML	Fri Apr 30 21:10:57 2010 +0200
+++ b/src/Pure/simplifier.ML	Fri Apr 30 23:33:42 2010 +0200
@@ -37,6 +37,7 @@
   val the_context: simpset -> Proof.context
   val context: Proof.context -> simpset -> simpset
   val global_context: theory  -> simpset -> simpset
+  val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
   val simproc_i: theory -> string -> term list
     -> (theory -> simpset -> term -> thm option) -> simproc
   val simproc: theory -> string -> string list