diff --git a/src/builtin/num.lean b/src/builtin/num.lean
index 98fab18ed9..5cff6efada 100644
--- a/src/builtin/num.lean
+++ b/src/builtin/num.lean
@@ -557,8 +557,6 @@ add_rewrite mul_onel mul_oner
 theorem mul_comm (a b : num) : a * b = b * a
 := induction_on b (by simp) (by simp)
 
-exit
-
 theorem distributer (a b c : num) : a * (b + c) = a * b + a * c
 := induction_on a (by simp) (by simp)
 
diff --git a/src/builtin/obj/num.olean b/src/builtin/obj/num.olean
index d5749bc9d7..6f986a4aef 100644
Binary files a/src/builtin/obj/num.olean and b/src/builtin/obj/num.olean differ