src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 50748 c056718eb687
parent 50747 a057d3fd6783
child 50823 0583db803066
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jan 05 22:31:30 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jan 05 22:31:30 2013 +0100
@@ -345,6 +345,11 @@
   member (op =) params_for_minimize name
 fun string_for_raw_param (key, values) =
   key ^ (case implode_param values of "" => "" | value => " = " ^ value)
+fun nice_string_for_raw_param (p as (key, ["false"])) =
+    (case AList.find (op =) negated_alias_params key of
+       [neg] => neg
+     | _ => string_for_raw_param p)
+  | nice_string_for_raw_param p = string_for_raw_param p
 
 fun minimize_command override_params i more_override_params prover_name
                      fact_names =
@@ -354,7 +359,7 @@
        |> filter_out (AList.defined (op =) more_override_params o fst)) @
       more_override_params
       |> filter is_raw_param_relevant_for_minimize
-      |> map string_for_raw_param
+      |> map nice_string_for_raw_param
       |> (if prover_name = default_minimize_prover then I else cons prover_name)
       |> space_implode ", "
   in