diff -r 0d46bea01741 -r a5fcf6d12a53 src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Thu Nov 08 20:08:00 2007 +0100
+++ b/src/HOL/Word/WordBitwise.thy	Thu Nov 08 20:08:01 2007 +0100
@@ -22,10 +22,10 @@
   word_and_def word_or_def word_xor_def
 
 lemmas word_no_log_defs [simp] = 
-  word_not_def  [where a="number_of ?a", 
-                 unfolded word_no_wi wils1, folded word_no_wi]
-  word_log_binary_defs [where a="number_of ?a" and b="number_of ?b",
-                        unfolded word_no_wi wils1, folded word_no_wi]
+  word_not_def  [where a="number_of a", 
+                 unfolded word_no_wi wils1, folded word_no_wi, standard]
+  word_log_binary_defs [where a="number_of a" and b="number_of b",
+                        unfolded word_no_wi wils1, folded word_no_wi, standard]
 
 lemmas word_wi_log_defs = word_no_log_defs [unfolded word_no_wi]