--- a/src/HOL/Number_Theory/Residues.thy	Mon Jul 22 22:55:19 2024 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Tue Jul 23 15:54:43 2024 +0100
@@ -283,8 +283,10 @@
   defines "R \<equiv> residue_ring (int p)"
 
 sublocale residues_prime < residues p
-  unfolding R_def residues_def
-  by (auto simp: p_prime prime_gt_1_int)
+proof
+  show "1 < int p"
+    using prime_gt_1_nat by auto
+qed
 
 context residues_prime
 begin