# 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) =