src/Pure/Proof/proof_syntax.ML
changeset 71288 06c6495fb1d0
parent 71286 4b45d592ce29
child 71993 3875815f5967
equal deleted inserted replaced
71287:907b7a6471a0 71288:06c6495fb1d0
   284 
   284 
   285 fun standard_proof_of {full, expand_name} thm =
   285 fun standard_proof_of {full, expand_name} thm =
   286   let val thy = Thm.theory_of_thm thm in
   286   let val thy = Thm.theory_of_thm thm in
   287     Thm.reconstruct_proof_of thm
   287     Thm.reconstruct_proof_of thm
   288     |> Proofterm.expand_proof thy expand_name
   288     |> Proofterm.expand_proof thy expand_name
   289     |> Proofterm.rew_proof thy
   289     |> Proofterm.rewrite_proof thy ([], Proof_Rewrite_Rules.rprocs true)
   290     |> Proofterm.no_thm_proofs
   290     |> Proofterm.no_thm_proofs
   291     |> not full ? Proofterm.shrink_proof
   291     |> not full ? Proofterm.shrink_proof
   292   end;
   292   end;
   293 
   293 
   294 fun pretty_standard_proof_of ctxt full thm =
   294 fun pretty_standard_proof_of ctxt full thm =