1.1 --- a/src/HOL/ex/Numeral.thy	Wed Apr 29 20:33:52 2009 -0700
     1.2 +++ b/src/HOL/ex/Numeral.thy	Thu Apr 30 07:33:40 2009 -0700
     1.3 @@ -257,16 +257,19 @@
     1.4  *}
     1.5  
     1.6  ML {*
     1.7 -fun mk_num 1 = @{term One}
     1.8 -  | mk_num k =
     1.9 -      let
    1.10 -        val (l, b) = Integer.div_mod k 2;
    1.11 -        val bit = (if b = 0 then @{term Dig0} else @{term Dig1});
    1.12 -      in bit $ (mk_num l) end;
    1.13 +fun mk_num k =
    1.14 +  if k > 1 then
    1.15 +    let
    1.16 +      val (l, b) = Integer.div_mod k 2;
    1.17 +      val bit = (if b = 0 then @{term Dig0} else @{term Dig1});
    1.18 +    in bit $ (mk_num l) end
    1.19 +  else if k = 1 then @{term One}
    1.20 +  else error ("mk_num " ^ string_of_int k);
    1.21  
    1.22  fun dest_num @{term One} = 1
    1.23    | dest_num (@{term Dig0} $ n) = 2 * dest_num n
    1.24 -  | dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1;
    1.25 +  | dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1
    1.26 +  | dest_num t = raise TERM ("dest_num", [t]);
    1.27  
    1.28  (*FIXME these have to gain proper context via morphisms phi*)
    1.29