--- a/src/Pure/more_thm.ML Fri Oct 11 21:44:39 2019 +0200
+++ b/src/Pure/more_thm.ML Fri Oct 11 21:51:10 2019 +0200
@@ -114,7 +114,7 @@
val untag: string -> attribute
val kind: string -> attribute
val reconstruct_proof_of: thm -> Proofterm.proof
- val clean_proof_of: bool -> thm -> Proofterm.proof
+ val standard_proof_of: bool -> thm -> Proofterm.proof
val register_proofs: thm list lazy -> theory -> theory
val consolidate_theory: theory -> unit
val show_consts: bool Config.T
@@ -656,16 +656,10 @@
fun reconstruct_proof_of thm =
Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
-fun clean_proof_of full thm =
- let
- val thy = Thm.theory_of_thm thm;
- val (_, prop) =
- Logic.unconstrainT (Thm.shyps_of thm)
- (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
- in
- Proofterm.strip_thm_proof (Thm.proof_of thm)
- |> Proofterm.reconstruct_proof thy prop
- |> Proofterm.expand_proof thy [("", NONE)]
+fun standard_proof_of full thm =
+ let val thy = Thm.theory_of_thm thm in
+ reconstruct_proof_of thm
+ |> Proofterm.expand_proof thy [("", NONE), (Thm.raw_derivation_name thm, NONE)]
|> Proofterm.rew_proof thy
|> Proofterm.no_thm_proofs
|> not full ? Proofterm.shrink_proof