From 97b3fd45ce5d4ecd12e10d077a5b4a3398ff9549 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 26 Jun 2015 19:14:36 -0700
Subject: [PATCH] fix(library/logic/axioms/prop_decidable): fixes #704

---
 library/logic/axioms/prop_decidable.lean | 4 ++--
 tests/lean/704.lean                      | 4 ++++
 tests/lean/704.lean.expected.out         | 2 ++
 3 files changed, 8 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/704.lean
 create mode 100644 tests/lean/704.lean.expected.out

diff --git a/library/logic/axioms/prop_decidable.lean b/library/logic/axioms/prop_decidable.lean
index 01d4f443f..3ba6df7cd 100644
--- a/library/logic/axioms/prop_decidable.lean
+++ b/library/logic/axioms/prop_decidable.lean
@@ -8,13 +8,13 @@ Excluded middle + Hilbert implies every proposition is decidable.
 import logic.axioms.prop_complete logic.axioms.hilbert data.sum
 open decidable inhabited nonempty sum
 
-theorem decidable_inhabited [instance] (a : Prop) : inhabited (decidable a) :=
+theorem decidable_inhabited [instance] [priority 0] (a : Prop) : inhabited (decidable a) :=
 inhabited_of_nonempty
   (or.elim (em a)
     (assume Ha, nonempty.intro (inl Ha))
     (assume Hna, nonempty.intro (inr Hna)))
 
-theorem prop_decidable [instance] (a : Prop) : decidable a :=
+theorem prop_decidable [instance] [priority 0] (a : Prop) : decidable a :=
 arbitrary (decidable a)
 
 theorem type_decidable (A : Type) : A + (A → false) :=
diff --git a/tests/lean/704.lean b/tests/lean/704.lean
new file mode 100644
index 000000000..36e74eef5
--- /dev/null
+++ b/tests/lean/704.lean
@@ -0,0 +1,4 @@
+import classical
+eval if true then 1 else 0
+attribute prop_decidable [priority 0]
+eval if true then 1 else 0
diff --git a/tests/lean/704.lean.expected.out b/tests/lean/704.lean.expected.out
new file mode 100644
index 000000000..6ed281c75
--- /dev/null
+++ b/tests/lean/704.lean.expected.out
@@ -0,0 +1,2 @@
+1
+1