src/Pure/Isar/isar_cmd.ML
changeset 61266 eb9522a9d997
parent 61144 5e94dfead1c2
child 62169 a6047f511de7
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Sep 25 19:28:33 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Sep 25 19:54:51 2015 +0200
     1.3 @@ -238,12 +238,12 @@
     1.4      Proof_Context.pretty_local_facts verbose (Toplevel.context_of st)
     1.5    else
     1.6      let
     1.7 -      val thy = Toplevel.theory_of st;
     1.8 +      val ctxt = Toplevel.context_of st;
     1.9        val prev_thys =
    1.10          (case Toplevel.previous_context_of st of
    1.11            SOME prev => [Proof_Context.theory_of prev]
    1.12 -        | NONE => Theory.parents_of thy);
    1.13 -    in Proof_Display.pretty_theorems_diff verbose prev_thys thy end;
    1.14 +        | NONE => Theory.parents_of (Proof_Context.theory_of ctxt));
    1.15 +    in Proof_Display.pretty_theorems_diff verbose prev_thys ctxt end;
    1.16  
    1.17  
    1.18  (* print theorems, terms, types etc. *)