# HG changeset patch
# User wenzelm
# Date 1125496007 -7200
# Node ID 49bc1bdc7b6e1f60145d4a5f94a77de4df3c258e
# Parent  19aa5ad633a7004ef2915f6f301af9ecd885f521
added no_body_context;

diff -r 19aa5ad633a7 -r 49bc1bdc7b6e src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Aug 31 15:46:46 2005 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Aug 31 15:46:47 2005 +0200
@@ -22,6 +22,7 @@
   val theory_of: state -> theory
   val sign_of: state -> theory    (*obsolete*)
   val body_context_of: state -> Proof.context
+  val no_body_context: state -> state
   val proof_of: state -> Proof.state
   val is_proof: state -> bool
   val enter_forward_proof: state -> Proof.state
@@ -149,6 +150,10 @@
     Theory (_, SOME ctxt) => ctxt
   | _ => node_case ProofContext.init Proof.context_of state);
 
+fun no_body_context (State NONE) = State NONE
+  | no_body_context (State (SOME (node, x))) =
+      State (SOME (History.apply (fn Theory (thy, _) => Theory (thy, NONE) | nd => nd) node, x));
+
 val proof_of = node_case (fn _ => raise UNDEF) I;
 val is_proof = can proof_of;