# HG changeset patch
# User haftmann
# Date 1156150961 -7200
# Node ID e2c6d096af01d3666883106bb8b72b9aa1be6808
# Parent  f01ae74f29f23f5d513486830d7202792266a9bb
more concise preprocessing of numerals for code generation

diff -r f01ae74f29f2 -r e2c6d096af01 src/HOL/Integ/IntArith.thy
--- 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;