src/Pure/Isar/isar_cmd.ML
changeset 67391 d55e52e25d9a
parent 67147 dea94b1aabc3
child 68823 5e7b1ae10eb8
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Jan 09 17:58:35 2018 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Jan 09 18:18:21 2018 +0100
     1.3 @@ -226,8 +226,8 @@
     1.4      let
     1.5        val ctxt = Toplevel.context_of st;
     1.6        val prev_thys =
     1.7 -        (case Toplevel.previous_context_of st of
     1.8 -          SOME prev => [Proof_Context.theory_of prev]
     1.9 +        (case Toplevel.previous_theory_of st of
    1.10 +          SOME thy => [thy]
    1.11          | NONE => Theory.parents_of (Proof_Context.theory_of ctxt));
    1.12      in Proof_Display.pretty_theorems_diff verbose prev_thys ctxt end;
    1.13