828 let val {thy=thyt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct |
828 let val {thy=thyt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct |
829 and {thy=thyu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu; |
829 and {thy=thyu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu; |
830 val maxi = Int.max(maxidx, Int.max(maxt, maxu)); |
830 val maxi = Int.max(maxidx, Int.max(maxt, maxu)); |
831 val thy' = Theory.merge(thy, Theory.merge(thyt, thyu)) |
831 val thy' = Theory.merge(thy, Theory.merge(thyt, thyu)) |
832 val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi) |
832 val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi) |
833 handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u]) |
833 handle Type.TUNIFY => raise TYPE ("Ill-typed instantiation:\nType\n" ^ |
|
834 Sign.string_of_typ thy' (Envir.norm_type tye T) ^ |
|
835 "\nof variable " ^ |
|
836 Sign.string_of_term thy' (Term.map_types (Envir.norm_type tye) t) ^ |
|
837 "\ncannot be unified with type\n" ^ |
|
838 Sign.string_of_typ thy' (Envir.norm_type tye U) ^ "\nof term " ^ |
|
839 Sign.string_of_term thy' (Term.map_types (Envir.norm_type tye) u), |
|
840 [T, U], [t, u]) |
834 in (thy', tye', maxi') end; |
841 in (thy', tye', maxi') end; |
835 in |
842 in |
836 fun cterm_instantiate [] th = th |
843 fun cterm_instantiate [] th = th |
837 | cterm_instantiate ctpairs0 th = |
844 | cterm_instantiate ctpairs0 th = |
838 let val (thy,tye,_) = List.foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0 |
845 let val (thy,tye,_) = List.foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0 |