@@ -1813,18 +1813,9 @@ collectDeferred top casenames ctxt (Bind n (GHole i t) app) =
1813 tidyArg env (Bind n b@(Pi im t k) sc)
1813 tidyArg env (Bind n b@(Pi im t k) sc)
1814 = Bind n (Pi im (tidy ctxt env t) k)
1814 = Bind n (Pi im (tidy ctxt env t) k)
1815 (tidyArg ((n, b) : env) sc)
1815 (tidyArg ((n, b) : env) sc)
1816− tidyArg env t = t
1816+ tidyArg env t = tidy ctxt env t
1818− tidy ctxt env t | (f, args) <- unApply t,
1819− P _ specn _ <- getFn f,
1820− n `notElem` casenames
1821− = normalise ctxt env t
1822− tidy ctxt env t@(Bind n (Let _ _) sct)
1823− | (f, args) <- unApply sct,
1824− P _ specn _ <- getFn f,
1825− n `notElem` casenames
1826− = normalise ctxt env t
1818+ tidy ctxt env t = normalise ctxt env t
1827− tidy ctxt env t = t
1829 getFn (Bind n (Lam _) t) = getFn t
1820 getFn (Bind n (Lam _) t) = getFn t
1830 getFn t | (f, a) <- unApply t = f
1821 getFn t | (f, a) <- unApply t = f