diff -r 6bec6daac280 -r e3a03f1f54eb src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Wed Jun 14 12:12:01 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy	Wed Jun 14 12:12:37 2006 +0200
@@ -781,13 +781,6 @@
 
 subsection {* code generator setup *}
 
-lemma number_of_eval [code fun]:
-  "number_of Numeral.Pls = (0::int)"
-  and "number_of Numeral.Min = uminus (1::int)"
-  and "number_of (n BIT bit.B0) = (2::int) * number_of n"
-  and "number_of (n BIT bit.B1) = (2::int) * number_of n + 1"
-  by simp_all
-
 lemma elim_nat [code unfolt]:
   "(number_of n :: nat) = nat (number_of n)"
   by simp
@@ -800,6 +793,10 @@
   "(1::int) = number_of (Numeral.Pls BIT bit.B1)" 
   by simp
 
+lemma elim_one_nat [code unfolt]:
+  "1 = Suc 0"
+  by simp
+
 lemmas [code unfolt] =
   bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
   bin_pred_Pls  bin_pred_Min  bin_pred_1  bin_pred_0