improved annotated type of equality in Nitpick's monotonicity check, based on a discovery by Alex
authorblanchet
Mon, 23 Nov 2009 13:23:39 +0100
changeset 33852 3a586209151e
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
--- 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) =