@@ -1813,18 +1813,9 @@ collectDeferred top casenames ctxt (Bind n (GHole i t) app) =
18131813 tidyArg env (Bind n b@(Pi im t k) sc)
18141814 = Bind n (Pi im (tidy ctxt env t) k)
18151815 (tidyArg ((n, b) : env) sc)
1816− tidyArg env t = t
1817−
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
1827− tidy ctxt env t = t
1816+ tidyArg env t = tidy ctxt env t
1817+
1818+ tidy ctxt env t = normalise ctxt env t
18281819
18291820 getFn (Bind n (Lam _) t) = getFn t
18301821 getFn t | (f, a) <- unApply t = f