# HG changeset patch
# User blanchet
# Date 1335463778 -7200
# Node ID 1678955ca991296a4b2cf0811e8cfcae3f0acef2
# Parent  49381b55b2c1a55912e1d37446e281a4830d2b64
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

diff -r 49381b55b2c1 -r 1678955ca991 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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