equal
deleted
inserted
replaced
220 let |
220 let |
221 val ctxt = fold_varnames Name.declare t Name.context; |
221 val ctxt = fold_varnames Name.declare t Name.context; |
222 val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys); |
222 val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys); |
223 in (vs_tys, t `$$ map (IVar o fst) vs_tys) end; |
223 in (vs_tys, t `$$ map (IVar o fst) vs_tys) end; |
224 |
224 |
225 fun eta_expand k (c as (_, (_, tys)), ts) = |
225 fun eta_expand k (c as (name, (_, tys)), ts) = |
226 let |
226 let |
227 val j = length ts; |
227 val j = length ts; |
228 val l = k - j; |
228 val l = k - j; |
|
229 val _ = if l > length tys |
|
230 then error ("Impossible eta-expansion for constant " ^ quote name) else (); |
229 val ctxt = (fold o fold_varnames) Name.declare ts Name.context; |
231 val ctxt = (fold o fold_varnames) Name.declare ts Name.context; |
230 val vs_tys = (map o apfst) SOME |
232 val vs_tys = (map o apfst) SOME |
231 (Name.names ctxt "a" ((take l o drop j) tys)); |
233 (Name.names ctxt "a" ((take l o drop j) tys)); |
232 in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end; |
234 in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end; |
233 |
235 |