src/HOL/Library/Efficient_Nat.thy

   using their counterparts on the integers:
 *}
 
 code_datatype number_nat_inst.number_of_nat
 
-lemma zero_nat_code [code, code unfold]:
+lemma zero_nat_code [code, code inline]:
   "0 = (Numeral0 :: nat)"
   by simp
 lemmas [code post] = zero_nat_code [symmetric]
 
-lemma one_nat_code [code, code unfold]:
+lemma one_nat_code [code, code inline]:
   "1 = (Numeral1 :: nat)"
   by simp
 lemmas [code post] = one_nat_code [symmetric]
 
 lemma Suc_code [code]:

   and @{term "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"} operations. *}
 
 definition
   divmod_aux ::  "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
 where
-  [code func del]: "divmod_aux = divmod"
-
-lemma [code func]:
+  [code del]: "divmod_aux = divmod"
+
+lemma [code]:
   "divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
   unfolding divmod_aux_def divmod_div_mod by simp
 
 lemma divmod_aux_code [code]:
   "divmod_aux n m = (nat (of_nat n div of_nat m), nat (of_nat n mod of_nat m))"

 text {*
   Case analysis on natural numbers is rephrased using a conditional
   expression:
 *}
 
-lemma [code func, code unfold]:
+lemma [code, code unfold]:
   "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
   by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc)
 
 
 subsection {* Preprocessors *}

     then remove_suc_clause thy ths else ths
   end;
 
 fun lift f thy eqns1 =
   let
-    val eqns2 = ((map o apfst) (AxClass.overload thy)
-      o burrow_fst Drule.zero_var_indexes_list) eqns1;
+    val eqns2 = burrow_fst Drule.zero_var_indexes_list eqns1;
     val thms3 = try (map fst
       #> map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
       #> f thy
       #> map (fn thm => thm RS @{thm eq_reflection})
       #> map (Conv.fconv_rule Drule.beta_eta_conversion)) eqns2;
     val thms4 = Option.map Drule.zero_var_indexes_list thms3;
   in case thms4
    of NONE => NONE
     | SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4)
-        then NONE else SOME (map (Code_Unit.mk_eqn thy) thms4)
+        then NONE else SOME (map (apfst (AxClass.overload thy) o Code_Unit.mk_eqn thy) thms4)
+          (*FIXME*)
   end
 
 in
 
   Codegen.add_preprocessor eqn_suc_preproc

   (SML "IntInf.< ((_), (_))")
   (OCaml "Big'_int.lt'_big'_int")
   (Haskell infix 4 "<")
 
 consts_code
-  0                            ("0")
+  "0::nat"                     ("0")
+  "1::nat"                     ("1")
   Suc                          ("(_ +/ 1)")
   "op + \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat"   ("(_ +/ _)")
   "op * \<Colon>  nat \<Rightarrow> nat \<Rightarrow> nat"   ("(_ */ _)")
   "op \<le> \<Colon>  nat \<Rightarrow> nat \<Rightarrow> bool"  ("(_ <=/ _)")
   "op < \<Colon>  nat \<Rightarrow> nat \<Rightarrow> bool"  ("(_ </ _)")