more concise preprocessing of numerals for code generation

--- a/src/HOL/Integ/IntArith.thy	Mon Aug 21 11:02:40 2006 +0200
+++ b/src/HOL/Integ/IntArith.thy	Mon Aug 21 11:02:41 2006 +0200
@@ -379,6 +379,15 @@
   "Numeral.B1" "IntDef.b1"
 
 lemma
+  Numeral_Pls_refl [code fun]: "Numeral.Pls = Numeral.Pls" ..
+
+lemma
+  Numeral_Min_refl [code fun]: "Numeral.Min = Numeral.Min" ..
+
+lemma
+  Numeral_Bit_refl [code fun]: "Numeral.Bit = Numeral.Bit" ..
+
+lemma
   number_of_is_rep_bin [code inline]: "number_of = Rep_Bin"
 proof
   fix b
@@ -415,7 +424,7 @@
 
 fun elim_negate thy thms =
   let
-    val thms' = map (rewrite_rule [number_of_is_rep_bin_thm]) thms;
+    val thms' = map (CodegenTheorems.rewrite_fun [number_of_is_rep_bin_thm]) thms;
     fun bins_of (Const _) =
           I
       | bins_of (Var _) =
@@ -441,8 +450,7 @@
       |> filter is_negative
       |> map instantiate_with
   in if null rewrites then thms' else
-    thms'
-    |> map (rewrite_rule rewrites)
+    map (CodegenTheorems.rewrite_fun rewrites) thms'
   end;
 
 end;