diff --git a/stage0/src/Init/Classical.lean b/stage0/src/Init/Classical.lean
index 720e3ce4c6..8efcfc1760 100644
--- a/stage0/src/Init/Classical.lean
+++ b/stage0/src/Init/Classical.lean
@@ -68,7 +68,7 @@ noncomputable def inhabitedOfExists {α : Sort u} {p : α → Prop} (h : ∃ x,
   inhabitedOfNonempty (Exists.elim h (fun w hw => ⟨w⟩))
 
 /- all propositions are Decidable -/
-noncomputable def propDecidable (a : Prop) : Decidable a :=
+@[scoped instance low] noncomputable def propDecidable (a : Prop) : Decidable a :=
   choice <| match em a with
     | Or.inl h => ⟨isTrue h⟩
     | Or.inr h => ⟨isFalse h⟩