# HG changeset patch
# User blanchet
# Date 1332200670 -3600
# Node ID ea6695d58aad8b32a28d690f473989f2ffa5eac1
# Parent  fc958d7138bed79d3fb37372b2083826fcbe6545
added "dont_preplay" alias

diff -r fc958d7138be -r ea6695d58aad src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Mar 20 00:44:30 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Mar 20 00:44:30 2012 +0100
@@ -8,7 +8,6 @@
 sig
   type params = Sledgehammer_Provers.params
 
-  val sledgehammerN : string
   val auto : bool Unsynchronized.ref
   val provers : string Unsynchronized.ref
   val timeout : int Unsynchronized.ref
@@ -29,9 +28,6 @@
 open Sledgehammer_Minimize
 open Sledgehammer_Run
 
-val sledgehammerN = "sledgehammer"
-val sledgehammer_paramsN = "sledgehammer_params"
-
 val runN = "run"
 val minN = "min"
 val messagesN = "messages"
@@ -101,7 +97,8 @@
    ("preplay_timeout", "3")]
 
 val alias_params =
-  [("prover", "provers")]
+  [("prover", ("provers", [])),
+   ("dont_preplay", ("preplay_timeout", ["0"]))]
 val negated_alias_params =
   [("no_debug", "debug"),
    ("quiet", "verbose"),
@@ -133,7 +130,13 @@
 
 fun unalias_raw_param (name, value) =
   case AList.lookup (op =) alias_params name of
-    SOME name' => (name', value)
+    SOME (name', []) => (name', value)
+  | SOME (param' as (name', _)) =>
+    if value <> ["false"] then
+      param'
+    else
+      error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \
+             \(cf. " ^ quote name' ^ ").")
   | NONE =>
     case AList.lookup (op =) negated_alias_params name of
       SOME name' => (name', case value of
@@ -340,7 +343,7 @@
       |> (if prover_name = default_minimize_prover then I else cons prover_name)
       |> space_implode ", "
   in
-    sledgehammerN ^ " " ^ minN ^
+    "sledgehammer" ^ " " ^ minN ^
     (if params = "" then "" else enclose " [" "]" params) ^
     " (" ^ space_implode " " fact_names ^ ")" ^
     (if i = 1 then "" else " " ^ string_of_int i)
@@ -434,6 +437,6 @@
                      (minimize_command [] i) state
   end
 
-val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer))
+val setup = Try.register_tool ("sledgehammer", (40, auto, try_sledgehammer))
 
 end;