diff -r 6410166400ea -r a21a96eda033 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 30 11:12:52 2019 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 30 11:41:39 2019 +0200
@@ -20,7 +20,7 @@
   | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
 
 fun prf_of ctxt thm =
-  Reconstruct.proof_of ctxt thm
+  Thm.reconstruct_proof_of ctxt thm
   |> Reconstruct.expand_proof ctxt [("", NONE)];  (* FIXME *)
 
 fun subsets [] = [[]]