514 let |
514 let |
515 val declared_outer = is_declared outer; |
515 val declared_outer = is_declared outer; |
516 val still_fixed = not o is_newly_fixed inner outer; |
516 val still_fixed = not o is_newly_fixed inner outer; |
517 |
517 |
518 val gen_fixes = |
518 val gen_fixes = |
519 Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? cons y) |
519 Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? Symtab.insert_set y) |
520 (fixes_of inner) []; |
520 (fixes_of inner) Symtab.empty; |
521 |
521 |
522 val type_occs_inner = type_occs_of inner; |
522 val type_occs_inner = type_occs_of inner; |
523 fun gen_fixesT ts = |
523 fun gen_fixesT ts = |
524 Symtab.fold (fn (a, xs) => |
524 Symtab.fold (fn (a, xs) => |
525 if declared_outer a orelse exists still_fixed xs |
525 if declared_outer a orelse exists still_fixed xs |
526 then I else cons a) (fold decl_type_occs ts type_occs_inner) []; |
526 then I else Symtab.insert_set a) (fold decl_type_occs ts type_occs_inner) Symtab.empty; |
527 in (gen_fixesT, gen_fixes) end; |
527 in (gen_fixesT, gen_fixes) end; |
528 |
528 |
529 fun exportT_inst inner outer = #1 (export_inst inner outer); |
529 fun exportT_inst inner outer = #1 (export_inst inner outer); |
530 |
530 |
531 fun exportT_terms inner outer = |
531 fun exportT_terms inner outer = |
532 let |
532 let |
533 val mk_tfrees = exportT_inst inner outer; |
533 val mk_tfrees = exportT_inst inner outer; |
534 val maxidx = maxidx_of outer; |
534 val maxidx = maxidx_of outer; |
535 in |
535 in |
536 fn ts => ts |> map |
536 fn ts => ts |> map |
537 (Term_Subst.generalize (Symtab.make_set (mk_tfrees ts), Symtab.empty) |
537 (Term_Subst.generalize (mk_tfrees ts, Symtab.empty) |
538 (fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1)) |
538 (fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1)) |
539 end; |
539 end; |
540 |
540 |
541 fun export_terms inner outer = |
541 fun export_terms inner outer = |
542 let |
542 let |
543 val (mk_tfrees, tfrees) = export_inst inner outer; |
543 val (mk_tfrees, tfrees) = export_inst inner outer; |
544 val maxidx = maxidx_of outer; |
544 val maxidx = maxidx_of outer; |
545 in |
545 in |
546 fn ts => ts |> map |
546 fn ts => ts |> map |
547 (Term_Subst.generalize (Symtab.make_set (mk_tfrees ts), Symtab.make_set tfrees) |
547 (Term_Subst.generalize (mk_tfrees ts, tfrees) |
548 (fold Term.maxidx_term ts maxidx + 1)) |
548 (fold Term.maxidx_term ts maxidx + 1)) |
549 end; |
549 end; |
550 |
550 |
551 fun export_prf inner outer prf = |
551 fun export_prf inner outer prf = |
552 let |
552 let |
553 val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer; |
553 val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer; |
554 val tfrees = Symtab.make_set (mk_tfrees []); |
554 val tfrees = mk_tfrees []; |
555 val maxidx = maxidx_of outer; |
555 val maxidx = maxidx_of outer; |
556 val idx = Proofterm.maxidx_proof prf maxidx + 1; |
556 val idx = Proofterm.maxidx_proof prf maxidx + 1; |
557 val gen_term = Term_Subst.generalize_same (tfrees, Symtab.make_set frees) idx; |
557 val gen_term = Term_Subst.generalize_same (tfrees, frees) idx; |
558 val gen_typ = Term_Subst.generalizeT_same tfrees idx; |
558 val gen_typ = Term_Subst.generalizeT_same tfrees idx; |
559 in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end; |
559 in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end; |
560 |
560 |
561 |
561 |
562 fun gen_export (mk_tfrees, frees) maxidx ths = |
562 fun gen_export (mk_tfrees, frees) maxidx ths = |
563 let |
563 let |
564 val tfrees = mk_tfrees (map Thm.full_prop_of ths); |
564 val tfrees = mk_tfrees (map Thm.full_prop_of ths); |
565 val idx = fold Thm.maxidx_thm ths maxidx + 1; |
565 val idx = fold Thm.maxidx_thm ths maxidx + 1; |
566 in map (Thm.generalize (Symtab.make_set tfrees, Symtab.make_set frees) idx) ths end; |
566 in map (Thm.generalize (tfrees, frees) idx) ths end; |
567 |
567 |
568 fun exportT inner outer = gen_export (exportT_inst inner outer, []) (maxidx_of outer); |
568 fun exportT inner outer = gen_export (exportT_inst inner outer, Symtab.empty) (maxidx_of outer); |
569 fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer); |
569 fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer); |
570 |
570 |
571 fun export_morphism inner outer = |
571 fun export_morphism inner outer = |
572 let |
572 let |
573 val fact = export inner outer; |
573 val fact = export inner outer; |