equal
deleted
inserted
replaced
237 val declare_typ = declare_term o Logic.mk_type; |
237 val declare_typ = declare_term o Logic.mk_type; |
238 |
238 |
239 val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type); |
239 val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type); |
240 |
240 |
241 val declare_thm = Thm.fold_terms declare_internal; |
241 val declare_thm = Thm.fold_terms declare_internal; |
242 fun global_thm_context th = declare_thm th (ProofContext.init_global (Thm.theory_of_thm th)); |
242 fun global_thm_context th = declare_thm th (Proof_Context.init_global (Thm.theory_of_thm th)); |
243 |
243 |
244 |
244 |
245 (* renaming term/type frees *) |
245 (* renaming term/type frees *) |
246 |
246 |
247 fun variant_frees ctxt ts frees = |
247 fun variant_frees ctxt ts frees = |
428 let val (inst, ctxt') = import_inst is_open ts ctxt |
428 let val (inst, ctxt') = import_inst is_open ts ctxt |
429 in (map (Term_Subst.instantiate inst) ts, ctxt') end; |
429 in (map (Term_Subst.instantiate inst) ts, ctxt') end; |
430 |
430 |
431 fun importT ths ctxt = |
431 fun importT ths ctxt = |
432 let |
432 let |
433 val thy = ProofContext.theory_of ctxt; |
433 val thy = Proof_Context.theory_of ctxt; |
434 val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; |
434 val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt; |
435 val insts' as (instT', _) = Thm.certify_inst thy (instT, []); |
435 val insts' as (instT', _) = Thm.certify_inst thy (instT, []); |
436 val ths' = map (Thm.instantiate insts') ths; |
436 val ths' = map (Thm.instantiate insts') ths; |
437 in ((instT', ths'), ctxt') end; |
437 in ((instT', ths'), ctxt') end; |
438 |
438 |
442 val (insts, ctxt') = import_inst is_open ts ctxt; |
442 val (insts, ctxt') = import_inst is_open ts ctxt; |
443 in (Proofterm.instantiate insts prf, ctxt') end; |
443 in (Proofterm.instantiate insts prf, ctxt') end; |
444 |
444 |
445 fun import is_open ths ctxt = |
445 fun import is_open ths ctxt = |
446 let |
446 let |
447 val thy = ProofContext.theory_of ctxt; |
447 val thy = Proof_Context.theory_of ctxt; |
448 val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt; |
448 val (insts, ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt; |
449 val insts' = Thm.certify_inst thy insts; |
449 val insts' = Thm.certify_inst thy insts; |
450 val ths' = map (Thm.instantiate insts') ths; |
450 val ths' = map (Thm.instantiate insts') ths; |
451 in ((insts', ths'), ctxt') end; |
451 in ((insts', ths'), ctxt') end; |
452 |
452 |