# HG changeset patch
# User wenzelm
# Date 1272663222 -7200
# Node ID 62d43ca574d0e6cefe34c216a1458515353b6bc4
# Parent  ca42a56e3b14976004c496a1fb987a87c42105c2
export Simplifier.with_context;

diff -r ca42a56e3b14 -r 62d43ca574d0 src/Pure/simplifier.ML
--- 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