diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 29a54c57bd..27adb9179a 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -8,6 +8,7 @@ import Lean.Elab.DeclUtil
 import Lean.Elab.Definition
 import Lean.Elab.Inductive
 import Lean.Elab.Structure
+import Lean.Elab.MutualDef
 
 namespace Lean
 namespace Elab
@@ -255,9 +256,6 @@ private def isMutualDef (stx : Syntax) : Bool :=
   declKind == `Lean.Parser.Command.abbrev ||
   declKind == `Lean.Parser.Command.theorem
 
-private def elabMutualDef (elems : Array Syntax) : CommandElabM Unit :=
-throwError "WIP mutual def"
-
 private def isMutualPreambleCommand (stx : Syntax) : Bool :=
 let k := stx.getKind;
 k == `Lean.Parser.Command.variable ||
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
new file mode 100644
index 0000000000..5a8c8ca8ac
--- /dev/null
+++ b/src/Lean/Elab/MutualDef.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.Command
+
+namespace Lean
+namespace Elab
+namespace Term
+
+def elabMutualDef (vars : Array Expr) (ds : Array Syntax) : TermElabM Unit := do
+throwError "WIP mutual def"
+
+end Term
+
+namespace Command
+
+def elabMutualDef (ds : Array Syntax) : CommandElabM Unit :=
+runTermElabM none fun vars => Term.elabMutualDef vars ds
+
+end Command
+end Elab
+end Lean