src/Pure/Isar/isar_cmd.ML
changeset 62922 96691631c1eb
parent 62913 13252110a6fe
child 63624 994d1a1105ef
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Apr 09 12:36:25 2016 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Apr 09 13:28:32 2016 +0200
     1.3 @@ -250,13 +250,12 @@
     1.4        NONE =>
     1.5          let
     1.6            val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
     1.7 -          val thy = Proof_Context.theory_of ctxt;
     1.8            val prf = Thm.proof_of thm;
     1.9            val prop = Thm.full_prop_of thm;
    1.10            val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
    1.11          in
    1.12            Proof_Syntax.pretty_proof ctxt
    1.13 -            (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
    1.14 +            (if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf')
    1.15          end
    1.16      | SOME srcs =>
    1.17          let val ctxt = Toplevel.context_of state