diff -r bf28f0179914 -r 6e34025981be src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 30 19:01:51 2019 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 30 20:09:25 2019 +0200
@@ -19,9 +19,11 @@
     [name] => name
   | _ => raise THM ("name_of_thm: bad proof of theorem", 0, [thm]));
 
-fun prf_of ctxt thm =
-  Thm.reconstruct_proof_of ctxt thm
-  |> Proofterm.expand_proof ctxt [("", NONE)];  (* FIXME *)
+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 subsets [] = [[]]
   | subsets (x::xs) =
@@ -257,7 +259,6 @@
 
 fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
   let
-    val ctxt = Proof_Context.init_global thy;
     val rvs = map fst (relevant_vars (Thm.prop_of rule));
     val xs = rev (Term.add_vars (Thm.prop_of rule) []);
     val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs);
@@ -269,7 +270,7 @@
     if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
     Extraction.abs_corr_shyps thy rule vs vs2
       (ProofRewriteRules.un_hhf_proof rlz' (attach_typeS rlz)
-         (fold_rev Proofterm.forall_intr_proof' rs (prf_of ctxt rrule)))))
+         (fold_rev Proofterm.forall_intr_proof' rs (prf_of thy rrule)))))
   end;
 
 fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));