src/Pure/Isar/toplevel.ML

   val is_toplevel: state -> bool
   val is_theory: state -> bool
   val is_proof: state -> bool
   val is_skipped_proof: state -> bool
   val level: state -> int
-  val previous_context_of: state -> Proof.context option
+  val previous_theory_of: state -> theory option
   val context_of: state -> Proof.context
   val generic_theory_of: state -> generic_theory
   val theory_of: state -> theory
   val proof_of: state -> Proof.state
   val proof_position_of: state -> int

 fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
 fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state);
 
 fun node_case f g state = cases_node f g (node_of state);
 
-fun previous_context_of (State (_, NONE)) = NONE
-  | previous_context_of (State (_, SOME prev)) = SOME (context_node prev);
+fun previous_theory_of (State (_, NONE)) = NONE
+  | previous_theory_of (State (_, SOME prev)) =
+      SOME (cases_node Context.theory_of Proof.theory_of prev);
 
 val context_of = node_case Context.proof_of Proof.context_of;
 val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
 val theory_of = node_case Context.theory_of Proof.theory_of;
 val proof_of = node_case (fn _ => error "No proof state") I;