diff --git a/library/init/classical.lean b/library/init/classical.lean
index ae3972fd1d..3bb9c5ba55 100644
--- a/library/init/classical.lean
+++ b/library/init/classical.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Jeremy Avigad
+Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 prelude
 import init.data.subtype.basic init.funext
@@ -11,7 +11,11 @@ namespace classical
 universes u v
 
 /- the axiom -/
-axiom indefinite_description {α : Sort u} (p : α → Prop) : (∃ x, p x) → {x // p x}
+axiom choice {α : Sort u} : nonempty α → α
+
+noncomputable theorem indefinite_description {α : Sort u} (p : α → Prop) :
+  (∃ x, p x) → {x // p x} :=
+λ h, choice (let ⟨x, px⟩ := h in ⟨⟨x, px⟩⟩)
 
 /- Diaconescu's theorem: using function extensionality and propositional extensionality,
    we can get excluded middle from this. -/
diff --git a/tests/lean/print_ax1.lean.expected.out b/tests/lean/print_ax1.lean.expected.out
index 7717d27b13..d17911a935 100644
--- a/tests/lean/print_ax1.lean.expected.out
+++ b/tests/lean/print_ax1.lean.expected.out
@@ -1,3 +1,3 @@
 quot.sound : ∀ {α : Type u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b
-classical.indefinite_description : Π {α : Sort u} (p : α → Prop), (∃ (x : α), p x) → {x // p x}
+classical.choice : Π {α : Sort u}, nonempty α → α
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out
index 7717d27b13..d17911a935 100644
--- a/tests/lean/print_ax2.lean.expected.out
+++ b/tests/lean/print_ax2.lean.expected.out
@@ -1,3 +1,3 @@
 quot.sound : ∀ {α : Type u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b
-classical.indefinite_description : Π {α : Sort u} (p : α → Prop), (∃ (x : α), p x) → {x // p x}
+classical.choice : Π {α : Sort u}, nonempty α → α
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
diff --git a/tests/lean/print_ax3.lean.expected.out b/tests/lean/print_ax3.lean.expected.out
index 80c513a615..d2436ea6e7 100644
--- a/tests/lean/print_ax3.lean.expected.out
+++ b/tests/lean/print_ax3.lean.expected.out
@@ -2,7 +2,7 @@ print_ax3.lean:13:6: warning: declaration 'foo5' uses sorry
 no axioms
 ------
 quot.sound : ∀ {α : Type u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b
-classical.indefinite_description : Π {α : Sort u} (p : α → Prop), (∃ (x : α), p x) → {x // p x}
+classical.choice : Π {α : Sort u}, nonempty α → α
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
 ------
 theorem foo3 : 0 = 0 :=