--- 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));