diff -r e939ea997f5f -r 7383930fc946 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Divides.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -811,7 +811,7 @@
   and less technical class hierarchy.
 \<close>
 
-class unique_euclidean_semiring_numeral = semiring_parity + linordered_semidom +
+class unique_euclidean_semiring_numeral = unique_euclidean_semiring_with_nat + linordered_semidom +
   assumes div_less: "0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a div b = 0"
     and mod_less: " 0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> a mod b = a"
     and div_positive: "0 < b \<Longrightarrow> b \<le> a \<Longrightarrow> a div b > 0"