diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index fd3bcb19d9..5ba5febacb 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -47,6 +47,9 @@ inductive False : Prop
 
 inductive Empty : Type
 
+set_option bootstrap.inductiveCheckResultingUniverse false in
+inductive PEmpty : Sort u where
+
 def Not (a : Prop) : Prop := a → False
 
 @[macroInline] def False.elim {C : Sort u} (h : False) : C :=
diff --git a/tests/lean/276.lean b/tests/lean/276.lean
index 2b75e92c30..36905318c8 100644
--- a/tests/lean/276.lean
+++ b/tests/lean/276.lean
@@ -1,9 +1,5 @@
 universe u v
 
--- `Type u` version can be defined without this option, but I get the same error
-set_option bootstrap.inductiveCheckResultingUniverse false in
-inductive PEmpty : Sort u
-
 -- `#check` works
 set_option pp.all true in
 #check fun {α : Sort v} => PEmpty.rec (fun _ => α)
diff --git a/tests/lean/276.lean.expected.out b/tests/lean/276.lean.expected.out
index ec3a1028b5..64df54df4d 100644
--- a/tests/lean/276.lean.expected.out
+++ b/tests/lean/276.lean.expected.out
@@ -1,2 +1,2 @@
 fun {α : Sort v} => PEmpty.rec.{v, u_1} fun (x : PEmpty.{u_1}) => α : {α : Sort v} → PEmpty.{u_1} → α
-276.lean:13:4-13:15: error: code generator does not support recursor 'PEmpty.rec' yet, consider using 'match ... with' and/or structural recursion
+276.lean:9:4-9:15: error: code generator does not support recursor 'PEmpty.rec' yet, consider using 'match ... with' and/or structural recursion