419 | prf_add_loose_bnos _ _ _ _ = ([], []); |
419 | prf_add_loose_bnos _ _ _ _ = ([], []); |
420 |
420 |
421 |
421 |
422 (**** substitutions ****) |
422 (**** substitutions ****) |
423 |
423 |
424 fun del_conflicting_tvars envT T = Term.instantiateT |
424 fun del_conflicting_tvars envT T = TermSubst.instantiateT |
425 (map_filter (fn ixnS as (_, S) => |
425 (map_filter (fn ixnS as (_, S) => |
426 (Type.lookup (envT, ixnS); NONE) handle TYPE _ => |
426 (Type.lookup (envT, ixnS); NONE) handle TYPE _ => |
427 SOME (ixnS, TFree ("'dummy", S))) (typ_tvars T)) T; |
427 SOME (ixnS, TFree ("'dummy", S))) (typ_tvars T)) T; |
428 |
428 |
429 fun del_conflicting_vars env t = Term.instantiate |
429 fun del_conflicting_vars env t = TermSubst.instantiate |
430 (map_filter (fn ixnS as (_, S) => |
430 (map_filter (fn ixnS as (_, S) => |
431 (Type.lookup (type_env env, ixnS); NONE) handle TYPE _ => |
431 (Type.lookup (type_env env, ixnS); NONE) handle TYPE _ => |
432 SOME (ixnS, TFree ("'dummy", S))) (term_tvars t), |
432 SOME (ixnS, TFree ("'dummy", S))) (term_tvars t), |
433 map_filter (fn Var (ixnT as (_, T)) => |
433 map_filter (fn Var (ixnT as (_, T)) => |
434 (Envir.lookup (env, ixnT); NONE) handle TYPE _ => |
434 (Envir.lookup (env, ixnT); NONE) handle TYPE _ => |
663 |
663 |
664 (***** generalization *****) |
664 (***** generalization *****) |
665 |
665 |
666 fun generalize (tfrees, frees) idx = |
666 fun generalize (tfrees, frees) idx = |
667 map_proof_terms_option |
667 map_proof_terms_option |
668 (Term.generalize_option (tfrees, frees) idx) |
668 (TermSubst.generalize_option (tfrees, frees) idx) |
669 (Term.generalizeT_option tfrees idx); |
669 (TermSubst.generalizeT_option tfrees idx); |
670 |
670 |
671 |
671 |
672 (***** instantiation *****) |
672 (***** instantiation *****) |
673 |
673 |
674 fun instantiate (instT, inst) = |
674 fun instantiate (instT, inst) = |
675 map_proof_terms_option |
675 map_proof_terms_option |
676 (Term.instantiate_option (instT, map (apsnd remove_types) inst)) |
676 (TermSubst.instantiate_option (instT, map (apsnd remove_types) inst)) |
677 (Term.instantiateT_option instT); |
677 (TermSubst.instantiateT_option instT); |
678 |
678 |
679 |
679 |
680 (***** lifting *****) |
680 (***** lifting *****) |
681 |
681 |
682 fun lift_proof Bi inc prop prf = |
682 fun lift_proof Bi inc prop prf = |