canonical approach towards lifting

--- a/src/HOL/ex/Bit_Lists.thy	Tue Feb 11 19:03:57 2020 +0100
+++ b/src/HOL/ex/Bit_Lists.thy	Thu Feb 13 07:43:48 2020 +0100
@@ -285,6 +285,8 @@
   "unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)"
   by (simp add: of_bits_int_def)
 
+unbundle word.lifting
+
 instantiation word :: (len) bit_representation
 begin
 
@@ -303,6 +305,9 @@
 
 end
 
+lifting_update word.lifting
+lifting_forget word.lifting
+
 
 subsection \<open>Bit representations with bit operations\<close>
 

--- a/src/HOL/ex/Word.thy	Tue Feb 11 19:03:57 2020 +0100
+++ b/src/HOL/ex/Word.thy	Thu Feb 13 07:43:48 2020 +0100
@@ -715,4 +715,7 @@
 
 end
 
+lifting_update word.lifting
+lifting_forget word.lifting
+
 end