diff -r 827bf668c822 -r c0304794e9e4 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Nov 17 12:29:48 2011 +0100
+++ b/src/HOL/Word/Word.thy	Thu Nov 17 12:38:03 2011 +0100
@@ -121,7 +121,7 @@
 
 subsection  "Arithmetic operations"
 
-instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, ord, bit}"
+instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, ord}"
 begin
 
 definition
@@ -157,22 +157,6 @@
 definition
   word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
 
-definition
-  word_and_def: 
-  "(a::'a word) AND b = word_of_int (uint a AND uint b)"
-
-definition
-  word_or_def:  
-  "(a::'a word) OR b = word_of_int (uint a OR uint b)"
-
-definition
-  word_xor_def: 
-  "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
-
-definition
-  word_not_def: 
-  "NOT (a::'a word) = word_of_int (NOT (uint a))"
-
 instance ..
 
 end
@@ -204,6 +188,22 @@
 begin
 
 definition
+  word_and_def: 
+  "(a::'a word) AND b = word_of_int (uint a AND uint b)"
+
+definition
+  word_or_def:  
+  "(a::'a word) OR b = word_of_int (uint a OR uint b)"
+
+definition
+  word_xor_def: 
+  "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
+
+definition
+  word_not_def: 
+  "NOT (a::'a word) = word_of_int (NOT (uint a))"
+
+definition
   word_test_bit_def: "test_bit a = bin_nth (uint a)"
 
 definition