diff -r bacfb7c45d81 -r 695cf1fab6cc src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 28 21:47:03 2015 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 28 23:14:40 2015 +0200
@@ -20,7 +20,7 @@
   | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
 
 fun prf_of thy thm =
-  Reconstruct.proof_of thm
+  Reconstruct.proof_of thy thm
   |> Reconstruct.expand_proof thy [("", NONE)];  (* FIXME *)
 
 fun subsets [] = [[]]