# HG changeset patch
# User huffman
# Date 1241102020 25200
# Node ID b5a35bfb3dabe1310fab95a784ac52fb4cd6c585
# Parent  020efcbfe2d84d8a37162947018437a883ecc972
detect error cases in mk_num, dest_num

diff -r 020efcbfe2d8 -r b5a35bfb3dab src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Wed Apr 29 20:33:52 2009 -0700
+++ b/src/HOL/ex/Numeral.thy	Thu Apr 30 07:33:40 2009 -0700
@@ -257,16 +257,19 @@
 *}
 
 ML {*
-fun mk_num 1 = @{term One}
-  | mk_num k =
-      let
-        val (l, b) = Integer.div_mod k 2;
-        val bit = (if b = 0 then @{term Dig0} else @{term Dig1});
-      in bit $ (mk_num l) end;
+fun mk_num k =
+  if k > 1 then
+    let
+      val (l, b) = Integer.div_mod k 2;
+      val bit = (if b = 0 then @{term Dig0} else @{term Dig1});
+    in bit $ (mk_num l) end
+  else if k = 1 then @{term One}
+  else error ("mk_num " ^ string_of_int k);
 
 fun dest_num @{term One} = 1
   | dest_num (@{term Dig0} $ n) = 2 * dest_num n
-  | dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1;
+  | dest_num (@{term Dig1} $ n) = 2 * dest_num n + 1
+  | dest_num t = raise TERM ("dest_num", [t]);
 
 (*FIXME these have to gain proper context via morphisms phi*)