diff -r a0ab0dc28d3c -r 3c587b7c3d5c src/HOL/Codegenerator_Test/Generate_Target_Nat.thy
--- a/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Tue Oct 26 16:22:03 2021 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Tue Oct 26 14:43:59 2021 +0000
@@ -16,6 +16,14 @@
   by a corresponding \<open>export_code\<close> command.
 \<close>
 
+lemma take_bit_num_code [code]: \<comment> \<open>TODO: move\<close>
+  \<open>take_bit_num n m = (case (n, m)
+   of (0, _) \<Rightarrow> None
+    | (Suc n, Num.One) \<Rightarrow> Some Num.One
+    | (Suc n, Num.Bit0 m) \<Rightarrow> (case take_bit_num n m of None \<Rightarrow> None | Some q \<Rightarrow> Some (Num.Bit0 q))
+    | (Suc n, Num.Bit1 m) \<Rightarrow> Some (case take_bit_num n m of None \<Rightarrow> Num.One | Some q \<Rightarrow> Num.Bit1 q))\<close>
+  by (cases n; cases m) simp_all
+
 export_code _ checking SML OCaml? Haskell? Scala
 
 end