# HG changeset patch
# User wenzelm
# Date 1137951960 -3600
# Node ID 7ff2934480c96dbeb569d1295da4e9d89962b1ca
# Parent  b38a18c9aed9492d5d9172d03f10bc8bd9e89f0c
added restore_body;

diff -r b38a18c9aed9 -r 7ff2934480c9 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Jan 22 18:45:59 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Jan 22 18:46:00 2006 +0100
@@ -14,6 +14,7 @@
   val theory_of: context -> theory
   val init: theory -> context
   val set_body: bool -> context -> context
+  val restore_body: context -> context -> context
   val assms_of: context -> term list
   val prems_of: context -> thm list
   val fact_index_of: context -> FactIndex.T
@@ -239,6 +240,7 @@
 
 val is_body = #1 o #fixes o rep_context;
 fun set_body b = map_fixes (fn (_, fixes) => (b, fixes));
+fun restore_body ctxt = set_body (is_body ctxt);
 
 val fixes_of = #2 o #fixes o rep_context;
 val fixed_names_of = map #2 o fixes_of;