improved annotated type of equality in Nitpick's monotonicity check, based on a discovery by Alex
authorblanchet
Mon Nov 23 13:23:39 2009 +0100 (2009-11-23)
changeset 338523a586209151e
parent 33851 ab6ecae44033
child 33853 348c3ea03e58
improved annotated type of equality in Nitpick's monotonicity check, based on a discovery by Alex
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Nov 23 13:22:40 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Nov 23 13:23:39 2009 +0100
     1.3 @@ -554,7 +554,8 @@
     1.4        end
     1.5      fun do_equals T (gamma, cset) =
     1.6        let val C = ctype_for (domain_type T) in
     1.7 -        (CFun (C, S Neg, CFun (C, S Neg, ctype_for (nth_range_type 2 T))),
     1.8 +        (CFun (C, S Neg, CFun (C, V (Unsynchronized.inc max_fresh),
     1.9 +                               ctype_for (nth_range_type 2 T))),
    1.10           (gamma, cset |> add_ctype_is_right_unique C))
    1.11        end
    1.12      fun do_robust_set_operation T (gamma, cset) =