diff -r 05c4c6a99b3f -r bd4d37edfee4 src/Pure/more_thm.ML
--- 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