diff -r bf39b07a7a8e -r d660c4b9daa6 src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Wed Nov 09 14:47:38 2011 +1100
+++ b/src/HOL/Numeral_Simprocs.thy	Wed Nov 09 10:58:08 2011 +0100
@@ -103,8 +103,8 @@
   {* fn phi => Numeral_Simprocs.combine_numerals *}
 
 simproc_setup field_combine_numerals
-  ("(i::'a::{field_inverse_zero, number_ring}) + j"
-  |"(i::'a::{field_inverse_zero, number_ring}) - j") =
+  ("(i::'a::{field_inverse_zero,ring_char_0,number_ring}) + j"
+  |"(i::'a::{field_inverse_zero,ring_char_0,number_ring}) - j") =
   {* fn phi => Numeral_Simprocs.field_combine_numerals *}
 
 simproc_setup inteq_cancel_numerals
@@ -141,8 +141,8 @@
   {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
 
 simproc_setup ring_eq_cancel_numeral_factor
-  ("(l::'a::{idom,number_ring}) * m = n"
-  |"(l::'a::{idom,number_ring}) = m * n") =
+  ("(l::'a::{idom,ring_char_0,number_ring}) * m = n"
+  |"(l::'a::{idom,ring_char_0,number_ring}) = m * n") =
   {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *}
 
 simproc_setup ring_less_cancel_numeral_factor
@@ -156,14 +156,14 @@
   {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *}
 
 simproc_setup int_div_cancel_numeral_factors
-  ("((l::'a::{semiring_div,number_ring}) * m) div n"
-  |"(l::'a::{semiring_div,number_ring}) div (m * n)") =
+  ("((l::'a::{semiring_div,ring_char_0,number_ring}) * m) div n"
+  |"(l::'a::{semiring_div,ring_char_0,number_ring}) div (m * n)") =
   {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
 
 simproc_setup divide_cancel_numeral_factor
-  ("((l::'a::{field_inverse_zero,number_ring}) * m) / n"
-  |"(l::'a::{field_inverse_zero,number_ring}) / (m * n)"
-  |"((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)") =
+  ("((l::'a::{field_inverse_zero,ring_char_0,number_ring}) * m) / n"
+  |"(l::'a::{field_inverse_zero,ring_char_0,number_ring}) / (m * n)"
+  |"((number_of v)::'a::{field_inverse_zero,ring_char_0,number_ring}) / (number_of w)") =
   {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
 
 simproc_setup ring_eq_cancel_factor