@@ -281,20 +281,11 @@ checkUnique borrowed ctxt env tm
281281 chkBinders env (App f a) = do chkBinders env f; chkBinders env a
282282 chkBinders env (Bind n b t)
283283 = do chkBinderName env n b
284− -- Must be safe whether we evaluate the scope or binder first
285− -- (Surely there is a tidier rule than this...?)
286284 st <- get
287− chkBinders env (binderTy b)
288285 case b of
289286 Let t v -> chkBinders env v
290287 _ -> return ()
291288 chkBinders ((n, b) : env) t
292−-- put st
293−-- chkBinders env (binderTy b)
294−-- case b of
295−-- Let t v -> chkBinders env v
296−-- _ -> return ()
297−-- chkBinders ((n, b) : env) t
298289 chkBinders env t = return ()
299290
300291 chkBinderName :: Env -> Name -> Binder Term ->