--- a/src/HOL/Tools/inductive_realizer.ML Sun Oct 20 16:16:23 2019 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Oct 20 20:38:22 2019 +0200
@@ -19,11 +19,10 @@
[name] => name
| _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
-fun prf_of thy raw_thm =
- let val thm = Thm.transfer thy raw_thm in
- Thm.reconstruct_proof_of thm
- |> Proofterm.expand_proof (Thm.theory_of_thm thm) [("", NONE)]
- end;
+fun prf_of thy =
+ Thm.transfer thy #>
+ Thm.reconstruct_proof_of #>
+ Proofterm.expand_proof thy Proofterm.expand_name_empty;
fun subsets [] = [[]]
| subsets (x::xs) =