diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index e8422eae35..8b878368dc 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -539,6 +539,11 @@ fun stx => failIfSucceeds stx $ elabCheck stx
 def addDecl (ref : Syntax) (decl : Declaration) : CommandElabM Unit := liftTermElabM none $ Term.addDecl ref decl
 def compileDecl (ref : Syntax) (decl : Declaration) : CommandElabM Unit := liftTermElabM none $ Term.compileDecl ref decl
 
+def addInstance (ref : Syntax) (declName : Name) : CommandElabM Unit := do
+env ← getEnv;
+env ← liftIO ref $ Meta.addGlobalInstance env declName;
+setEnv env
+
 unsafe def elabEvalUnsafe : CommandElab :=
 fun stx => withoutModifyingEnv do
   let ref  := stx;
diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index fe42f1a245..f0f6fd08f2 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -162,11 +162,6 @@ attrs.forM $ fun attr => do
      env ← liftIO ref $ attrImpl.add env declName attr.args true;
      setEnv env
 
-def addInstance (ref : Syntax) (declName : Name) : CommandElabM Unit := do
-env ← getEnv;
-env ← liftIO ref $ Meta.addGlobalInstance env declName;
-setEnv env
-
 end Command
 end Elab
 end Lean
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index c0fe68123d..6729f5cd6b 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -989,6 +989,17 @@ match env.compileDecl opts decl with
 | Except.ok env    => setEnv env
 | Except.error kex => throwError ref (kex.toMessageData opts)
 
+def mkAuxDefinition (ref : Syntax) (declName : Name) (type : Expr) (value : Expr) : TermElabM Expr := do
+env ← getEnv;
+opts ← getOptions;
+mctx ← getMCtx;
+lctx ← getLCtx;
+match Lean.mkAuxDefinition env opts mctx lctx declName type value with
+| Except.error ex    => throwError ref (ex.toMessageData opts)
+| Except.ok (r, env) => do
+  setEnv env;
+  pure r
+
 private partial def mkAuxNameAux (env : Environment) (base : Name) : Nat → Name
 | i =>
   let candidate := base.appendIndexAfter i;