diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 28dba32e2c..cf1399d982 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Elab.Quotation.Precheck
 import Lean.Elab.Term
+import Lean.Elab.BindersUtil
 import Lean.Parser.Term
 
 namespace Lean.Elab.Term
@@ -101,19 +102,6 @@ private def getBinderIds (ids : Syntax) : TermElabM (Array Syntax) :=
     else
       throwErrorAt id "identifier or `_` expected"
 
-/-
-  Recall that
-  ```
-  def typeSpec := leading_parser " : " >> termParser
-  def optType : Parser := optional typeSpec
-  ```
--/
-def expandOptType (ref : Syntax) (optType : Syntax) : Syntax :=
-  if optType.isNone then
-    mkHole ref
-  else
-    optType[0][1]
-
 private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) := do
   let k := stx.getKind
   if k == `Lean.Parser.Term.simpleBinder then
diff --git a/src/Lean/Elab/BindersUtil.lean b/src/Lean/Elab/BindersUtil.lean
new file mode 100644
index 0000000000..9247ba043f
--- /dev/null
+++ b/src/Lean/Elab/BindersUtil.lean
@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+namespace Lean.Elab.Term
+/-
+  Recall that
+  ```
+  def typeSpec := leading_parser " : " >> termParser
+  def optType : Parser := optional typeSpec
+  ```
+-/
+def expandOptType (ref : Syntax) (optType : Syntax) : Syntax :=
+  if optType.isNone then
+    mkHole ref
+  else
+    optType[0][1]
+
+end Lean.Elab.Term
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index a6d1c14fbf..f690b69a4e 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Elab.Term
-import Lean.Elab.Binders
+import Lean.Elab.BindersUtil
 import Lean.Elab.PatternVar
 import Lean.Elab.Quotation.Util
 import Lean.Parser.Do