# 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