285 if occurs(F,t,env) then (ocheck_fail(F,t,binders,env); raise Unif) |
285 if occurs(F,t,env) then (ocheck_fail(F,t,binders,env); raise Unif) |
286 else (let val (u,env') = proj(t,env,binders,is) |
286 else (let val (u,env') = proj(t,env,binders,is) |
287 in Envir.update((F,mkabs(binders,is,u)),env') end |
287 in Envir.update((F,mkabs(binders,is,u)),env') end |
288 handle Unif => (proj_fail params; raise Unif)); |
288 handle Unif => (proj_fail params; raise Unif)); |
289 |
289 |
290 fun unify(sg,env,tus) = (sgr := sg; tsgr := #tsig(Sign.rep_sg sg); |
290 fun unify(sg,env,tus) = (sgr := sg; tsgr := Sign.tsig_of sg; |
291 foldl (unif []) (env,tus)); |
291 foldl (unif []) (env,tus)); |
292 |
292 |
293 |
293 |
294 (*Eta-contract a term (fully)*) |
294 (*Eta-contract a term (fully)*) |
295 |
295 |