@@ -414,7 +414,7 @@ buildDepMap ci used externs ctx startNames
414414 V i -> snd (bs !! i) cd `union` unconditionalDeps args
415415
416416 -- we interpret applied lambdas as lets in order to reuse code here
417− Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet [] app)
417+ Bind n (Lam ty) t -> getDepsTerm vs bs cd (lamToLet app)
418418
419419 -- and we interpret applied lets as lambdas
420420 Bind n ( Let ty t') t -> getDepsTerm vs bs cd (App Complete (Bind n (Lam ty) t) t')
@@ -491,11 +491,8 @@ buildDepMap ci used externs ctx startNames
491491
492492 -- convert applications of lambdas to lets
493493 -- Note that this transformation preserves de bruijn numbering
494− lamToLet :: [Term] -> Term -> Term
495− lamToLet xs (App _ f x) = lamToLet (x:xs) f
496− lamToLet (x:xs) (Bind n (Lam ty) t) = Bind n (Let ty x) (lamToLet xs t)
497− lamToLet (x:xs) t = App Complete (lamToLet xs t) x
498− lamToLet [] t = t
494+ lamToLet :: Term -> Term
495+ lamToLet (App _ (Bind n (Lam ty) tm) val) = Bind n (Let ty val) tm
499496
500497 -- split "\x_i -> T(x_i)" into [x_i] and T
501498 unfoldLams :: Term -> ([Name], Term)