# HG changeset patch
# User haftmann
# Date 1172846604 -3600
# Node ID 9859d69101eb6f28da337a27c76ae7b647d5382d
# Parent  35f54980d4cc28974fed10b17f974edb2276830e
simplified code generator setup

diff -r 35f54980d4cc -r 9859d69101eb src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Fri Mar 02 15:43:23 2007 +0100
+++ b/src/HOL/Integ/NatBin.thy	Fri Mar 02 15:43:24 2007 +0100
@@ -813,54 +813,8 @@
 
 subsection {* code generator setup *}
 
-lemma neg_number_of_Pls:
-  "\<not> neg ((number_of Numeral.Pls) \<Colon> int)"
-  by auto
-
-lemma neg_number_of_Min:
-  "neg ((number_of Numeral.Min) \<Colon> int)"
-  by auto
-
-lemmas nat_number_expand = nat_number Let_def if_bool_eq_conj if_True if_False
-  neg_number_of_Pls neg_number_of_Min neg_number_of_BIT Nat.plus.simps
-
-ML {*
-structure NumeralNat =
-struct
-
-val nat_number_expand = thms "nat_number_expand";
+lemmas [code inline] = nat_number_of_def
 
-fun elim_number_of_nat thy ts =
-  let
-    fun bins_of (Const _) =
-          I
-      | bins_of (Var _) =
-          I
-      | bins_of (Free _) =
-          I
-      | bins_of (Bound _) =
-          I
-      | bins_of (Abs (_, _, t)) =
-          bins_of t
-      | bins_of (t as _ $ _) =
-          case strip_comb t
-           of (Const ("Numeral.number_of",
-               Type (_, [_, Type ("nat", [])])), _) => cons t
-            | (t', ts) => bins_of t' #> fold bins_of ts;
-    val simpset =
-      HOL_basic_ss addsimps nat_number_expand;
-  in
-    []
-    |> fold (bins_of o Thm.term_of) ts
-    |> map (Simplifier.rewrite simpset o Thm.cterm_of thy)
-  end;
-
-end;
-*}
-
-setup {*
-  CodegenData.add_inline_proc ("elim_number_of_nat", NumeralNat.elim_number_of_nat)
-*}
 
 subsection {* legacy ML bindings *}