diff -r 274b4edca859 -r a4e82b58d833 src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Numeral_Simprocs.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -169,8 +169,8 @@
 
 (* TODO: remove comm_ring_1 constraint if possible *)
 simproc_setup int_div_cancel_numeral_factors
-  ("((l::'a::{semiring_div,comm_ring_1,ring_char_0}) * m) div n"
-  |"(l::'a::{semiring_div,comm_ring_1,ring_char_0}) div (m * n)") =
+  ("((l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) * m) div n"
+  |"(l::'a::{euclidean_semiring_cancel,comm_ring_1,ring_char_0}) div (m * n)") =
   \<open>fn phi => Numeral_Simprocs.div_cancel_numeral_factor\<close>
 
 simproc_setup divide_cancel_numeral_factor
@@ -194,13 +194,13 @@
   \<open>fn phi => Numeral_Simprocs.less_cancel_factor\<close>
 
 simproc_setup int_div_cancel_factor
-  ("((l::'a::semiring_div) * m) div n"
-  |"(l::'a::semiring_div) div (m * n)") =
+  ("((l::'a::euclidean_semiring_cancel) * m) div n"
+  |"(l::'a::euclidean_semiring_cancel) div (m * n)") =
   \<open>fn phi => Numeral_Simprocs.div_cancel_factor\<close>
 
 simproc_setup int_mod_cancel_factor
-  ("((l::'a::semiring_div) * m) mod n"
-  |"(l::'a::semiring_div) mod (m * n)") =
+  ("((l::'a::euclidean_semiring_cancel) * m) mod n"
+  |"(l::'a::euclidean_semiring_cancel) mod (m * n)") =
   \<open>fn phi => Numeral_Simprocs.mod_cancel_factor\<close>
 
 simproc_setup dvd_cancel_factor