279 fun unify thy = unif thy []; |
279 fun unify thy = unif thy []; |
280 |
280 |
281 |
281 |
282 (* put a term into eta long beta normal form *) |
282 (* put a term into eta long beta normal form *) |
283 fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t) |
283 fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t) |
284 | eta_long Ts t = (case strip_comb t of |
284 | eta_long Ts t = |
285 (Abs _, _) => eta_long Ts (Envir.beta_norm t) |
285 (case strip_comb t of |
286 | (u, ts) => |
286 (Abs _, _) => eta_long Ts (Envir.beta_norm t) |
287 let |
287 | (u, ts) => |
288 val Us = binder_types (fastype_of1 (Ts, t)); |
288 let |
289 val i = length Us |
289 val Us = binder_types (fastype_of1 (Ts, t)); |
290 in list_abs (map (pair "x") Us, |
290 val i = length Us; |
291 list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts)) |
291 in |
292 (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0)))) |
292 fold_rev (Term.abs o pair "x") Us |
293 end); |
293 (list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts)) |
|
294 (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0)))) |
|
295 end); |
294 |
296 |
295 |
297 |
296 (*Tests whether 2 terms are alpha/eta-convertible and have same type. |
298 (*Tests whether 2 terms are alpha/eta-convertible and have same type. |
297 Note that Consts and Vars may have more than one type.*) |
299 Note that Consts and Vars may have more than one type.*) |
298 fun t aeconv u = t aconv u orelse |
300 fun t aeconv u = t aconv u orelse |