src/HOL/Library/Numeral_Type.thy

--- a/src/HOL/Library/Numeral_Type.thy	Fri Sep 30 21:03:58 2022 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Sat Oct 01 07:56:53 2022 +0000
@@ -156,7 +156,7 @@
 by (rule type_definition.Abs_inverse [OF type])
 
 lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n"
-by (simp add: Abs_inverse pos_mod_conj [OF size0])
+  using size0 by (simp add: Abs_inverse)
 
 lemma Rep_Abs_0: "Rep (Abs 0) = 0"
 by (simp add: Abs_inverse size0)