# HG changeset patch
# User blanchet
# Date 1258979019 -3600
# Node ID 3a586209151ea6d333249dc03f5836fb57b2769f
# Parent  ab6ecae440333bd18fdeea27f689411dee46f50d
improved annotated type of equality in Nitpick's monotonicity check, based on a discovery by Alex

diff -r ab6ecae44033 -r 3a586209151e src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Nov 23 13:22:40 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Nov 23 13:23:39 2009 +0100
@@ -554,7 +554,8 @@
       end
     fun do_equals T (gamma, cset) =
       let val C = ctype_for (domain_type T) in
-        (CFun (C, S Neg, CFun (C, S Neg, ctype_for (nth_range_type 2 T))),
+        (CFun (C, S Neg, CFun (C, V (Unsynchronized.inc max_fresh),
+                               ctype_for (nth_range_type 2 T))),
          (gamma, cset |> add_ctype_is_right_unique C))
       end
     fun do_robust_set_operation T (gamma, cset) =