src/HOL/Library/Efficient_Nat.thy

 *)
 
 header {* Implementation of natural numbers by integers *}
 
 theory Efficient_Nat
-imports Main Code_Integer
+imports Main Code_Integer Code_Index
 begin
 
 text {*
 When generating code for functions on natural numbers, the canonical
 representation using @{term "0::nat"} and @{term "Suc"} is unsuitable for

   shows "number_of k = nat_of_int (number_of k)"
   unfolding nat_of_int_def [OF assms] nat_number_of_def number_of_is_id ..
 
 lemma nat_of_int_of_number_of_aux:
   fixes k
-  assumes "Numeral.Pls \<le> k \<equiv> True"
+  assumes "Int.Pls \<le> k \<equiv> True"
   shows "k \<ge> 0"
   using assms unfolding Pls_def by simp
 
 lemma nat_of_int_int:
   "nat_of_int (int_of_nat n) = n"

   let
     val simplify_less = Simplifier.rewrite 
       (HOL_basic_ss addsimps (@{thms less_numeral_code} @ @{thms less_eq_numeral_code}));
     fun mk_rew (t, ty) =
       if ty = HOLogic.natT andalso 0 <= HOLogic.dest_numeral t then
-        Thm.capply @{cterm "(op \<le>) Numeral.Pls"} (Thm.cterm_of thy t)
+        Thm.capply @{cterm "(op \<le>) Int.Pls"} (Thm.cterm_of thy t)
         |> simplify_less
         |> (fn thm => @{thm nat_of_int_of_number_of_aux} OF [thm])
         |> (fn thm => @{thm nat_of_int_of_number_of} OF [thm])
         |> (fn thm => @{thm eq_reflection} OF [thm])
         |> SOME

 
 
 subsection {* Module names *}
 
 code_modulename SML
+  Int Integer
   Nat Integer
   Divides Integer
   Efficient_Nat Integer
 
 code_modulename OCaml
+  Int Integer
   Nat Integer
   Divides Integer
   Efficient_Nat Integer
 
 code_modulename Haskell
+  Int Integer
   Nat Integer
   Divides Integer
   Efficient_Nat Integer
 
 hide const nat_of_int int_of_nat