# HG changeset patch
# User bulwahn
# Date 1290418924 -3600
# Node ID 99c6ce92669be4d3469025277814406453e35c8c
# Parent  5615cc557120500e6d81d609ec0e905249006df9
added useful function map_context_result to signature

diff -r 5615cc557120 -r 99c6ce92669b src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Nov 22 10:42:03 2010 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Nov 22 10:42:04 2010 +0100
@@ -16,6 +16,7 @@
   val context_of: state -> context
   val theory_of: state -> theory
   val map_context: (context -> context) -> state -> state
+  val map_context_result : (context -> 'a * context) -> state -> 'a * state
   val map_contexts: (context -> context) -> state -> state
   val propagate_ml_env: state -> state
   val bind_terms: (indexname * term option) list -> state -> state