added restore_body;
authorwenzelm
Sun, 22 Jan 2006 18:46:00 +0100
changeset 18743 7ff2934480c9
parent 18742 b38a18c9aed9
child 18744 a9a5ee0e43e2
added restore_body;
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;