# HG changeset patch
# User blanchet
# Date 1271256625 -7200
# Node ID 08b2a7ecb6c3349ff8ee504fcb55dad86973be41
# Parent  c210a8fda4c5a0c5c904377a643d498265c472f8
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
and added "atp" as alias for "atps"

diff -r c210a8fda4c5 -r 08b2a7ecb6c3 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 11:24:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 16:50:25 2010 +0200
@@ -51,7 +51,9 @@
    ("sorts", "false"),
    ("minimize_timeout", "5 s")]
 
-val negated_params =
+val alias_params =
+  [("atp", "atps")]
+val negated_alias_params =
   [("no_debug", "debug"),
    ("quiet", "verbose"),
    ("ignore_no_atp", "respect_no_atp"),
@@ -66,21 +68,25 @@
 
 fun is_known_raw_param s =
   AList.defined (op =) default_default_params s orelse
-  AList.defined (op =) negated_params s orelse
+  AList.defined (op =) alias_params s orelse
+  AList.defined (op =) negated_alias_params s orelse
   member (op =) property_dependent_params s
 
 fun check_raw_param (s, _) =
   if is_known_raw_param s then ()
   else error ("Unknown parameter: " ^ quote s ^ ".")
 
-fun unnegate_raw_param (name, value) =
-  case AList.lookup (op =) negated_params name of
-    SOME name' => (name', case value of
-                            ["false"] => ["true"]
-                          | ["true"] => ["false"]
-                          | [] => ["false"]
-                          | _ => value)
-  | NONE => (name, value)
+fun unalias_raw_param (name, value) =
+  case AList.lookup (op =) alias_params name of
+    SOME name' => (name', value)
+  | NONE =>
+    case AList.lookup (op =) negated_alias_params name of
+      SOME name' => (name', case value of
+                              ["false"] => ["true"]
+                            | ["true"] => ["false"]
+                            | [] => ["false"]
+                            | _ => value)
+    | NONE => (name, value)
 
 structure Data = Theory_Data(
   type T = raw_param list
@@ -88,19 +94,20 @@
   val extend = I
   fun merge p : T = AList.merge (op =) (K true) p)
 
-val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
+val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
 fun default_raw_params thy =
-  [("atps", [!atps]),
-   ("full_types", [if !full_types then "true" else "false"]),
-   ("timeout", [string_of_int (!timeout) ^ " s"])] @
   Data.get thy
+  |> fold (AList.default (op =))
+          [("atps", [!atps]),
+           ("full_types", [if !full_types then "true" else "false"]),
+           ("timeout", [string_of_int (!timeout) ^ " s"])]
 
 val infinity_time_in_secs = 60 * 60 * 24 * 365
 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
 
 fun extract_params thy default_params override_params =
   let
-    val override_params = map unnegate_raw_param override_params
+    val override_params = map unalias_raw_param override_params
     val raw_params = rev override_params @ rev default_params
     val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
     val lookup_string = the_default "" o lookup
diff -r c210a8fda4c5 -r 08b2a7ecb6c3 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 14 11:24:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 14 16:50:25 2010 +0200
@@ -550,7 +550,7 @@
   | minimize_line name xs =
       "To minimize the number of lemmas, try this command: " ^
       Markup.markup Markup.sendback
-                    ("sledgehammer minimize [atps = " ^ name ^ "] (" ^
+                    ("sledgehammer minimize [atp = " ^ name ^ "] (" ^
                      space_implode " " xs ^ ")") ^ ".\n"
 
 fun metis_lemma_list dfg name (result as (_, _, _, _, goal, i)) =