diff -r ff9efdc84289 -r bdc835d934b7 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Mon Apr 22 06:28:17 2019 +0000
+++ b/src/HOL/Word/Word.thy	Mon Apr 22 09:33:55 2019 +0000
@@ -358,7 +358,14 @@
 
 subsection \<open>Bit-wise operations\<close>
 
-instantiation word :: (len0) bits
+definition shiftl1 :: "'a::len0 word \<Rightarrow> 'a word"
+  where "shiftl1 w = word_of_int (uint w BIT False)"
+
+definition shiftr1 :: "'a::len0 word \<Rightarrow> 'a word"
+  \<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close>
+  where "shiftr1 w = word_of_int (bin_rest (uint w))"
+
+instantiation word :: (len0) bit_operations
 begin
 
 lift_definition bitNOT_word :: "'a word \<Rightarrow> 'a word" is bitNOT
@@ -383,13 +390,6 @@
 
 definition "msb a \<longleftrightarrow> bin_sign (sbintrunc (LENGTH('a) - 1) (uint a)) = - 1"
 
-definition shiftl1 :: "'a word \<Rightarrow> 'a word"
-  where "shiftl1 w = word_of_int (uint w BIT False)"
-
-definition shiftr1 :: "'a word \<Rightarrow> 'a word"
-  \<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close>
-  where "shiftr1 w = word_of_int (bin_rest (uint w))"
-
 definition shiftl_def: "w << n = (shiftl1 ^^ n) w"
 
 definition shiftr_def: "w >> n = (shiftr1 ^^ n) w"