src/HOL/Library/Efficient_Nat.thy

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

   "op * \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat"   ("(_ */ _)")
   "op \<le> \<Colon>  nat \<Rightarrow> nat \<Rightarrow> bool"  ("(_ <=/ _)")
   "op < \<Colon>  nat \<Rightarrow> nat \<Rightarrow> bool"  ("(_ </ _)")
 
 
+text {* Evaluation *}
+
+lemma [code func, code func del]:
+  "(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
+
+code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
+  (SML "HOLogic.mk'_number/ HOLogic.natT")
+
+
 text {* Module names *}
 
 code_modulename SML
   Nat Integer
   Divides Integer