fixed bug in handling of new numerals -- the left-hand side of "Numeral1 = 1" should be left alone and not translated to a built-in Kodkod numeral in the specification of the "numeral" function

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Apr 26 19:44:18 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Apr 26 20:09:38 2012 +0200
@@ -1642,14 +1642,20 @@
          let
            val j = mult * (HOLogic.dest_num t1)
                    |> T = nat_T ? Integer.max 0
-           val s = numeral_prefix ^ signed_string_of_int j
          in
-           if is_integer_like_type T then
-             if is_standard_datatype thy stds T then Const (s, T)
-             else funpow j (curry (op $) (suc_const T)) (zero_const T)
+           if j = 1 then
+             raise SAME ()
            else
-             do_term depth Ts (Const (@{const_name of_int}, int_T --> T)
-                               $ Const (s, int_T))
+             let
+               val s = numeral_prefix ^ signed_string_of_int j
+             in
+               if is_integer_like_type T then
+                 if is_standard_datatype thy stds T then Const (s, T)
+                 else funpow j (curry (op $) (suc_const T)) (zero_const T)
+               else
+                 do_term depth Ts (Const (@{const_name of_int}, int_T --> T)
+                                   $ Const (s, int_T))
+             end
          end
          handle TERM _ => raise SAME ()
        else