src/Pure/Isar/isar_cmd.ML

--- 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;