equal
deleted
inserted
replaced
248 Pretty.string_of |
248 Pretty.string_of |
249 (case arg of |
249 (case arg of |
250 NONE => |
250 NONE => |
251 let |
251 let |
252 val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state); |
252 val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state); |
253 val thy = Proof_Context.theory_of ctxt; |
|
254 val prf = Thm.proof_of thm; |
253 val prf = Thm.proof_of thm; |
255 val prop = Thm.full_prop_of thm; |
254 val prop = Thm.full_prop_of thm; |
256 val prf' = Proofterm.rewrite_proof_notypes ([], []) prf; |
255 val prf' = Proofterm.rewrite_proof_notypes ([], []) prf; |
257 in |
256 in |
258 Proof_Syntax.pretty_proof ctxt |
257 Proof_Syntax.pretty_proof ctxt |
259 (if full then Reconstruct.reconstruct_proof thy prop prf' else prf') |
258 (if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf') |
260 end |
259 end |
261 | SOME srcs => |
260 | SOME srcs => |
262 let val ctxt = Toplevel.context_of state |
261 let val ctxt = Toplevel.context_of state |
263 in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end |
262 in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end |
264 |> Pretty.chunks); |
263 |> Pretty.chunks); |