author | bulwahn |
Mon, 22 Nov 2010 10:42:04 +0100 | |
changeset 40642 | 99c6ce92669b |
parent 40641 | 5615cc557120 |
child 40643 | 3bba5e71a873 |
--- 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