diff -r 40fdd74b75f3 -r 85fb1a585f52 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Apr 16 19:50:19 2019 +0000
+++ b/src/HOL/Word/Word.thy	Tue Apr 16 19:50:20 2019 +0000
@@ -62,7 +62,7 @@
 
 definition sint :: "'a::len word \<Rightarrow> int"
   \<comment> \<open>treats the most-significant-bit as a sign bit\<close>
-  where sint_uint: "sint w = sbintrunc (len_of TYPE('a) - 1) (uint w)"
+  where sint_uint: "sint w = sbintrunc (LENGTH('a) - 1) (uint w)"
 
 definition unat :: "'a::len0 word \<Rightarrow> nat"
   where "unat w = nat (uint w)"
@@ -377,10 +377,12 @@
 
 definition word_set_bit_def: "set_bit a n x = word_of_int (bin_sc n x (uint a))"
 
-definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE('a)) f)"
+definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth LENGTH('a) f)"
 
 definition word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
 
+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)"
 
@@ -396,6 +398,10 @@
 
 end
 
+lemma word_msb_def:
+  "msb a \<longleftrightarrow> bin_sign (sint a) = - 1"
+  by (simp add: msb_word_def sint_uint)
+
 lemma [code]:
   shows word_not_def: "NOT (a::'a::len0 word) = word_of_int (NOT (uint a))"
     and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)"
@@ -403,15 +409,6 @@
     and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
   by (simp_all add: bitNOT_word_def bitAND_word_def bitOR_word_def bitXOR_word_def)
 
-instantiation word :: (len) bitss
-begin
-
-definition word_msb_def: "msb a \<longleftrightarrow> bin_sign (sint a) = -1"
-
-instance ..
-
-end
-
 definition setBit :: "'a::len0 word \<Rightarrow> nat \<Rightarrow> 'a word"
   where "setBit w n = set_bit w n True"