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