786 Vartab.fold (fn (xi, (S, T)) => |
786 Vartab.fold (fn (xi, (S, T)) => |
787 cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv []; |
787 cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv []; |
788 val inst = args' |> map (fn ((xi, T), cu) => |
788 val inst = args' |> map (fn ((xi, T), cu) => |
789 ((xi, Envir.norm_type tyenv T), |
789 ((xi, Envir.norm_type tyenv T), |
790 Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu))); |
790 Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu))); |
791 in instantiate_normalize (instT, inst) th end; |
791 in instantiate_normalize (instT, inst) th end |
|
792 handle CTERM (msg, _) => raise THM (msg, 0, [th]) |
|
793 | TERM (msg, _) => raise THM (msg, 0, [th]) |
|
794 | TYPE (msg, _, _) => raise THM (msg, 0, [th]); |
792 |
795 |
793 (*Left-to-right replacements: tpairs = [..., (vi, ti), ...]. |
796 (*Left-to-right replacements: tpairs = [..., (vi, ti), ...]. |
794 Instantiates distinct Vars by terms, inferring type instantiations.*) |
797 Instantiates distinct Vars by terms, inferring type instantiations.*) |
795 local |
798 local |
796 fun add_types (ct, cu) (thy, tye, maxidx) = |
799 fun add_types (ct, cu) (thy, tye, maxidx) = |