diff --git a/library/init/core.lean b/library/init/core.lean
index d1f672c11f..3baa39d6a9 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -317,6 +317,11 @@ inductive nat
 | zero : nat
 | succ (n : nat) : nat
 
+/- Auxiliary axiom used to implement `sorry`.
+   TODO: add this theorem on-demand. That is,
+   we should only add it if after the first error. -/
+constant sorry_ax (α : Sort u) (synthetic := tt) : α
+
 /- Declare builtin and reserved notation -/
 
 class has_zero     (α : Type u) := (zero : α)
@@ -2169,8 +2174,3 @@ theorem by_contradiction {p : Prop} (h : ¬p → false) : p :=
 decidable.by_contradiction h
 
 end classical
-
-/- Auxiliary axiom used to implement `sorry`.
-   TODO: add this theorem on-demand. That is,
-   we should only add it if after the first error. -/
-constant sorry_ax (α : Sort u) (synthetic := tt) : α