# HG changeset patch
# User blanchet
# Date 1291638789 -3600
# Node ID 60d931de07098fcaf51f78f73a67572c04f4448a
# Parent  01f33bf79596a74cf21696031a476f1e293ef29e
fixed quantifier handling of new monotonicity calculus

diff -r 01f33bf79596 -r 60d931de0709 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
@@ -559,7 +559,7 @@
        |> map swap
        |> AList.group (op =)
        |> map (fn (a, xs) => string_for_annotation a ^ ": " ^
-                             string_for_vars ", " xs)
+                             string_for_vars ", " (sort int_ord xs))
        |> space_implode "\n"))
 
 fun solve max_var (comps, clauses) =
@@ -1044,7 +1044,7 @@
             fun ann () = if quant_s = @{const_name Ex} then Fls else Tru
             val (body_m, accum) =
               accum ||> side_cond
-                        ? add_mtype_is_complete [(x, (Minus, ann ()))] abs_M
+                        ? add_mtype_is_complete [(x, (Plus, ann ()))] abs_M
                     |>> push_bound (V x) abs_T abs_M |> do_formula sn body_t
             val body_M = mtype_of_mterm body_m
           in