# HG changeset patch # User wenzelm # Date 1272663614 -7200 # Node ID 8a041e2d812273d90d916bb88673cd81ced154a5 # Parent 62d43ca574d0e6cefe34c216a1458515353b6bc4 map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.; diff -r 62d43ca574d0 -r 8a041e2d8122 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Fri Apr 30 23:33:42 2010 +0200 +++ b/src/Provers/clasimp.ML Fri Apr 30 23:40:14 2010 +0200 @@ -70,8 +70,14 @@ fun get_css context = (Classical.get_cs context, Simplifier.get_ss context); fun map_css f context = - let val (cs', ss') = f (get_css context) - in context |> Classical.map_cs (K cs') |> Simplifier.map_ss (K ss') end; + let + val (cs, ss) = get_css context; + val (cs', ss') = f (cs, Simplifier.context (Context.proof_of context) ss); + in + context + |> Classical.map_cs (K cs') + |> Simplifier.map_ss (K (Simplifier.inherit_context ss ss')) + end; fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt);