224 val Hty = type_of_G env (Fty,length is,map (idx is) ks) |
224 val Hty = type_of_G env (Fty,length is,map (idx is) ks) |
225 val (env',H) = Envir.genvar a (env,Hty) |
225 val (env',H) = Envir.genvar a (env,Hty) |
226 fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks)); |
226 fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks)); |
227 in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env')) |
227 in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env')) |
228 end; |
228 end; |
229 in if TermOrd.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end |
229 in if Term_Ord.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end |
230 |
230 |
231 fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) = |
231 fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) = |
232 if T = U then env |
232 if T = U then env |
233 else |
233 else |
234 let val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx) |
234 let val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx) |