--- a/src/Pure/more_thm.ML Sun Oct 20 16:16:23 2019 +0200
+++ b/src/Pure/more_thm.ML Sun Oct 20 20:38:22 2019 +0200
@@ -114,7 +114,8 @@
val untag: string -> attribute
val kind: string -> attribute
val reconstruct_proof_of: thm -> Proofterm.proof
- val standard_proof_of: {full: bool, expand: string list} -> thm -> Proofterm.proof
+ val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
+ thm -> Proofterm.proof
val register_proofs: thm list lazy -> theory -> theory
val consolidate_theory: theory -> unit
val show_consts: bool Config.T
@@ -656,10 +657,10 @@
fun reconstruct_proof_of thm =
Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
-fun standard_proof_of {full, expand} thm =
+fun standard_proof_of {full, expand_name} thm =
let val thy = Thm.theory_of_thm thm in
reconstruct_proof_of thm
- |> Proofterm.expand_proof thy (map (rpair NONE) ("" :: expand))
+ |> Proofterm.expand_proof thy expand_name
|> Proofterm.rew_proof thy
|> Proofterm.no_thm_proofs
|> not full ? Proofterm.shrink_proof