diff -r 23df00d48d6f -r 3f875966c3e1 src/HOL/Library/Tools/word_lib.ML --- a/src/HOL/Library/Tools/word_lib.ML Sun Mar 30 11:21:34 2025 +0200 +++ b/src/HOL/Library/Tools/word_lib.ML Sun Mar 30 13:50:06 2025 +0200 @@ -35,7 +35,7 @@ then Type (\<^type_name>\Numeral_Type.bit0\, [T]) else Type (\<^type_name>\Numeral_Type.bit1\, [T]) -fun mk_binT size = +fun mk_binT size = if size = 0 then \<^typ>\Numeral_Type.num0\ else if size = 1 then \<^typ>\Numeral_Type.num1\ else let val (q, r) = Integer.div_mod size 2 in mk_bitT r (mk_binT q) end