# HG changeset patch
# User blanchet
# Date 1291638789 -3600
# Node ID 117345744f44e0363cd311aafe925fa149760d90
# Parent  e5a23ffb5524d331b72cddc27d9a582c85146c53
fixed bug in monotonicity solution display, whereby the polarity of literals was ignored

diff -r e5a23ffb5524 -r 117345744f44 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
@@ -309,7 +309,7 @@
       | _ => MType (simple_string_of_typ T, [])
   in do_type end
 
-val ground_and_sole_base_constrs = [@{const_name Nil}, @{const_name None}]
+val ground_and_sole_base_constrs = [] (* FIXME: [@{const_name Nil}, @{const_name None}], cf. lists_empty *)
 
 fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
   | prodM_factors M = [M]
@@ -579,7 +579,8 @@
 
 fun solve tac_timeout max_var (comps, clauses) =
   let
-    val asgs = map_filter (fn [(x, (_, a))] => SOME (x, a) | _ => NONE) clauses
+    val asgs =
+      map_filter (fn [(x, (Plus, a))] => SOME (x, a) | _ => NONE) clauses
     fun do_assigns assigns =
       SOME (extract_assigns max_var assigns asgs |> tap print_solution)
     val _ = print_problem comps clauses