src/HOL/Library/Numeral_Type.thy

--- a/src/HOL/Library/Numeral_Type.thy	Sun Mar 11 13:39:16 2012 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Sun Mar 11 13:54:08 2012 +0100
@@ -135,8 +135,8 @@
 
 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