diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr
index e0edbdadf..f7118ed7c 100644
--- a/src/Idris/Elab/Implementation.idr
+++ b/src/Idris/Elab/Implementation.idr
@@ -185,7 +185,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
                fns <- topMethTypes [] impName methImps impsp (params cdata)
                                       (map fst (methods cdata))
                                       (methods cdata)
-               traverse (processDecl [] nest env) (map mkTopMethDecl fns)
+               traverse_ (processDecl [] nest env) (map mkTopMethDecl fns)
 
                -- 3. Build the record for the implementation
                let mtops = map (Builtin.fst . snd) fns
diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr
index b0e2e8897..ba1f55ca4 100644
--- a/src/TTImp/Elab/Case.idr
+++ b/src/TTImp/Elab/Case.idr
@@ -226,7 +226,15 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
          -- Start with empty nested names, since we've extended the rhs with
          -- ICaseLocal so they'll get rebuilt with the right environment
          let nest' = MkNested []
+         ust <- get UST
+         -- We don't want to keep rechecking delayed elaborators in the
+         -- case block, because they're not going to make progress until
+         -- we come out again, so save them
+         let olddelayed = delayedElab ust
+         put UST (record { delayedElab = [] } ust)
          processDecl [InCase] nest' [] (IDef fc casen alts')
+         ust <- get UST
+         put UST (record { delayedElab = olddelayed } ust)
 
          pure (appTm, gnf env caseretty)
   where
diff --git a/src/TTImp/Elab/Delayed.idr b/src/TTImp/Elab/Delayed.idr
index 5f076dd6b..0438449f0 100644
--- a/src/TTImp/Elab/Delayed.idr
+++ b/src/TTImp/Elab/Delayed.idr
@@ -71,7 +71,7 @@ delayOnFailure fc rig env expected pred pri elab
          handle (elab False)
           (\err =>
               do est <- get EST
-                 if pred err && delayDepth est < !getAmbigLimit
+                 if pred err
                     then
                       do nm <- genName "delayed"
                          (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
@@ -99,19 +99,16 @@ delayElab : {vars : _} ->
             Core (Term vars, Glued vars)
 delayElab {vars} fc rig env exp pri elab
     = do est <- get EST
-         if delayDepth est >= !getAmbigLimit
-            then elab
-            else do
-             nm <- genName "delayed"
-             expected <- mkExpected exp
-             (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
-             logGlueNF 5 ("Postponing elaborator " ++ show nm ++
-                          " for") env expected
-             ust <- get UST
-             put UST (record { delayedElab $=
-                     ((pri, ci, mkClosedElab fc env (deeper elab)) :: ) }
-                             ust)
-             pure (dtm, expected)
+         nm <- genName "delayed"
+         expected <- mkExpected exp
+         (ci, dtm) <- newDelayed fc linear env nm !(getTerm expected)
+         logGlueNF 5 ("Postponing elaborator " ++ show nm ++
+                      " for") env expected
+         ust <- get UST
+         put UST (record { delayedElab $=
+                 ((pri, ci, mkClosedElab fc env elab) :: ) }
+                         ust)
+         pure (dtm, expected)
   where
     mkExpected : Maybe (Glued vars) -> Core (Glued vars)
     mkExpected (Just ty) = pure ty
@@ -196,7 +193,6 @@ retryDelayed : {vars : _} ->
 retryDelayed ds
     = do est <- get EST
          ds <- retryDelayed' NoError [] ds -- try everything again
-         ds <- retryDelayed' AmbigError [] ds -- fail on ambiguity error
          retryDelayed' AllErrors [] ds -- fail on all errors
          pure ()
 
diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr
index 2cb0e6337..917f4590e 100644
--- a/src/TTImp/Elab/Local.idr
+++ b/src/TTImp/Elab/Local.idr
@@ -37,7 +37,15 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty
                                            -- fixes bug #115
          let nest' = record { names $= (names' ++) } nest
          let env' = dropLinear env
+         -- We don't want to keep rechecking delayed elaborators in the
+         -- locals  block, because they're not going to make progress until
+         -- we come out again, so save them
+         ust <- get UST
+         let olddelayed = delayedElab ust
+         put UST (record { delayedElab = [] } ust)
          traverse (processDecl [] nest' env') (map (updateName nest') nestdecls)
+         ust <- get UST
+         put UST (record { delayedElab = olddelayed } ust)
          check rig elabinfo nest' env scope expty
   where
     -- For the local definitions, don't allow access to linear things