src/Pure/Isar/toplevel.ML

   val node_of: state -> node
   val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
   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
   val prompt_state_default: state -> string
   val prompt_state_fn: (state -> string) ref

 fun body_context_of state =
   (case node_of state of
     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;
 
 val enter_forward_proof = node_case Proof.init Proof.enter_forward;