diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 8f48b6d6eb..99ce562743 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -155,8 +155,6 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
     throwError! "expected type must not contain free or meta variables{indentExpr expectedType}"
   return expectedType
 
-#exit -- TODO remove after update stage0
-
 @[builtinTactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun stx =>
   closeMainUsing fun expectedType => do
     let expectedType ← preprocessPropToDecide expectedType