clarified signature;

--- a/src/Pure/Isar/isar_cmd.ML	Tue Jan 09 17:58:35 2018 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Jan 09 18:18:21 2018 +0100
@@ -226,8 +226,8 @@
     let
       val ctxt = Toplevel.context_of st;
       val prev_thys =
-        (case Toplevel.previous_context_of st of
-          SOME prev => [Proof_Context.theory_of prev]
+        (case Toplevel.previous_theory_of st of
+          SOME thy => [thy]
         | NONE => Theory.parents_of (Proof_Context.theory_of ctxt));
     in Proof_Display.pretty_theorems_diff verbose prev_thys ctxt end;
 

--- a/src/Pure/Isar/toplevel.ML	Tue Jan 09 17:58:35 2018 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Jan 09 18:18:21 2018 +0100
@@ -15,7 +15,7 @@
   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
@@ -153,8 +153,9 @@
 
 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);