diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 30643577c2..9649752ced 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -293,6 +293,4 @@ TODO
 @[builtinTermElab] def elabsubst : TermElab := expandInfixOp infixR " ▸ " 75
 -/
 
-end Term
-end Elab
-end Lean
+end Lean.Elab.Term
diff --git a/src/Lean/Elab/CollectFVars.lean b/src/Lean/Elab/CollectFVars.lean
index 98fe1a38dc..3b1952d21b 100644
--- a/src/Lean/Elab/CollectFVars.lean
+++ b/src/Lean/Elab/CollectFVars.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -6,36 +7,31 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 import Lean.Util.CollectFVars
 import Lean.Elab.Term
 
-namespace Lean
-namespace Elab
-namespace Term
-
+namespace Lean.Elab.Term
 open Meta
 
 def collectUsedFVars (e : Expr) : StateRefT CollectFVars.State TermElabM Unit := do
-e ← instantiateMVars e;
+let e ← instantiateMVars e
 modify fun used => collectFVars used e
 
 def collectUsedFVarsAtFVars (fvars : Array Expr) : StateRefT CollectFVars.State TermElabM Unit :=
 fvars.forM fun fvar => do
-  fvarType ← inferType fvar;
+  let fvarType ← inferType fvar
   collectUsedFVars fvarType
 
 def removeUnused (vars : Array Expr) (used : CollectFVars.State) : TermElabM (LocalContext × LocalInstances × Array Expr) := do
-localInsts ← getLocalInstances;
-lctx ← getLCtx;
-(lctx, localInsts, newVars, _) ← vars.foldrM
-  (fun var (result : LocalContext × LocalInstances × Array Expr × CollectFVars.State) =>
-    let (lctx, localInsts, newVars, used) := result;
-    if used.fvarSet.contains var.fvarId! then do
-      varType ← inferType var;
-      (_, used) ← (collectUsedFVars varType).run used;
+let localInsts ← getLocalInstances
+let lctx ← getLCtx
+let (lctx, localInsts, newVars, _) ← vars.foldrM
+  (fun var (result : LocalContext × LocalInstances × Array Expr × CollectFVars.State) => do
+    let (lctx, localInsts, newVars, used) := result
+    if used.fvarSet.contains var.fvarId! then
+      let varType ← inferType var
+      let (_, used) ← (collectUsedFVars varType).run used
       pure (lctx, localInsts, newVars.push var, used)
     else
       pure (lctx.erase var.fvarId!, localInsts.erase var.fvarId!, newVars, used))
-  (lctx, localInsts, #[], used);
+  (lctx, localInsts, #[], used)
 pure (lctx, localInsts, newVars.reverse)
 
-end Term
-end Elab
-end Lean
+end Lean.Elab.Term