tuned

--- a/src/HOL/Numeral.thy	Thu Jul 19 21:47:39 2007 +0200
+++ b/src/HOL/Numeral.thy	Thu Jul 19 21:47:42 2007 +0200
@@ -210,7 +210,7 @@
 axclass number_ring \<subseteq> number, comm_ring_1
   number_of_eq: "number_of k = of_int k"
 
-text {* self-embedding of the intergers *}
+text {* self-embedding of the integers *}
 
 instance int :: number_ring
   int_number_of_def: "number_of w \<equiv> of_int w"
@@ -589,36 +589,36 @@
 code_datatype Pls Min Bit "number_of \<Colon> int \<Rightarrow> int"
 
 definition
-  int_aux :: "int \<Rightarrow> nat \<Rightarrow> int" where
-  "int_aux i n = (i + int n)"
+  int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
+  "int_aux n i = int n + i"
 
 lemma [code]:
-  "int_aux i 0 = i"
-  "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
+  "int_aux 0 i  = i"
+  "int_aux (Suc n) i = int_aux n (i + 1)" -- {* tail recursive *}
   by (simp add: int_aux_def)+
 
 lemma [code unfold]:
-  "int n = int_aux 0 n"
+  "int n = int_aux n 0"
   by (simp add: int_aux_def)
 
 definition
-  nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat" where
-  "nat_aux n i = (n + nat i)"
+  nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
+  "nat_aux i n = nat i + n"
 
-lemma [code]: "nat_aux n i = (if i <= 0 then n else nat_aux (Suc n) (i - 1))"
-  -- {* tail recursive *}
+lemma [code]:
+  "nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))"  -- {* tail recursive *}
   by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
     dest: zless_imp_add1_zle)
 
-lemma [code]: "nat i = nat_aux 0 i"
+lemma [code]: "nat i = nat_aux i 0"
   by (simp add: nat_aux_def)
 
 lemma zero_is_num_zero [code func, code inline, symmetric, normal post]:
-  "(0\<Colon>int) = number_of Numeral.Pls" 
+  "(0\<Colon>int) = Numeral0" 
   by simp
 
 lemma one_is_num_one [code func, code inline, symmetric, normal post]:
-  "(1\<Colon>int) = number_of (Numeral.Pls BIT bit.B1)" 
+  "(1\<Colon>int) = Numeral1" 
   by simp 
 
 code_modulename SML

--- a/src/HOL/Tools/Qelim/qelim.ML	Thu Jul 19 21:47:39 2007 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Thu Jul 19 21:47:42 2007 +0200
@@ -2,8 +2,7 @@
     ID:         $Id$
     Author:     Amine Chaieb and Tobias Nipkow, TU Muenchen
 
-Proof protocoling and proof generation for multiple quantified
-formulae.
+Proof protocolling and proof generation for multiple quantified formulae.
 *)
 
 signature QELIM =

--- a/src/Pure/Tools/codegen_consts.ML	Thu Jul 19 21:47:39 2007 +0200
+++ b/src/Pure/Tools/codegen_consts.ML	Thu Jul 19 21:47:42 2007 +0200
@@ -30,6 +30,7 @@
     -> string * typ list -> const
   val consts_of_cos: theory -> string -> (string * sort) list
     -> (string * typ list) list -> const list
+  val no_args: theory -> const -> int
 
   val typargs: theory -> string * typ -> typ list
   val typ_sort_inst: Sorts.algebra -> typ * sort
@@ -159,7 +160,7 @@
     val (c, _) = const;
     val ty = (Logic.unvarifyT o mg_typ_of_const thy) const;
     fun err () = raise BAD
-     ("Illegal type for datatype constructor: " ^ string_of_typ thy ty);
+      ("Illegal type for datatype constructor: " ^ string_of_typ thy ty);
     val (tys, ty') = strip_type ty;
     val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty'
       handle TYPE _ => err ();
@@ -178,6 +179,8 @@
 fun co_of_const thy const = gen_co_of_const thy const handle BAD msg => error msg;
 fun co_of_const' thy const = SOME (gen_co_of_const thy const) handle BAD msg => NONE;
 
+fun no_args thy = length o fst o strip_type o mg_typ_of_const thy;
+
 end;
 
 fun cos_of_consts thy consts =

--- a/src/Pure/Tools/codegen_data.ML	Thu Jul 19 21:47:39 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Thu Jul 19 21:47:42 2007 +0200
@@ -139,7 +139,7 @@
       | matches (_ :: _) [] = false
       | matches (x :: xs) (y :: ys) = Pattern.matches thy (x, y) andalso matches xs ys;
     fun drop thm' = not (matches args (args_of thm'))
-      orelse (warning ("Dropping redundant defining equation\n" ^ string_of_thm thm'); false);
+      orelse (warning ("code generator: dropping redundant defining equation\n" ^ string_of_thm thm'); false);
     val (keeps, drops) = List.partition drop sels;
   in (thm :: keeps, dels |> remove Thm.eq_thm_prop thm |> fold (insert Thm.eq_thm_prop) drops) end;