src/HOL/Library/Numeral_Type.thy

 apply (simp_all add: Rep_simps zmod_simps field_simps)
 done
 
 end
 
-locale mod_ring = mod_type +
-  constrains n :: int
+locale mod_ring = mod_type n Rep Abs
+  for n :: int
   and Rep :: "'a::{number_ring} \<Rightarrow> int"
   and Abs :: "int \<Rightarrow> 'a::{number_ring}"
 begin
 
 lemma of_nat_eq: "of_nat k = Abs (int k mod n)"