1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Mar 20 00:44:30 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Mar 20 00:44:30 2012 +0100
     1.3 @@ -8,7 +8,6 @@
     1.4  sig
     1.5    type params = Sledgehammer_Provers.params
     1.6  
     1.7 -  val sledgehammerN : string
     1.8    val auto : bool Unsynchronized.ref
     1.9    val provers : string Unsynchronized.ref
    1.10    val timeout : int Unsynchronized.ref
    1.11 @@ -29,9 +28,6 @@
    1.12  open Sledgehammer_Minimize
    1.13  open Sledgehammer_Run
    1.14  
    1.15 -val sledgehammerN = "sledgehammer"
    1.16 -val sledgehammer_paramsN = "sledgehammer_params"
    1.17 -
    1.18  val runN = "run"
    1.19  val minN = "min"
    1.20  val messagesN = "messages"
    1.21 @@ -101,7 +97,8 @@
    1.22     ("preplay_timeout", "3")]
    1.23  
    1.24  val alias_params =
    1.25 -  [("prover", "provers")]
    1.26 +  [("prover", ("provers", [])),
    1.27 +   ("dont_preplay", ("preplay_timeout", ["0"]))]
    1.28  val negated_alias_params =
    1.29    [("no_debug", "debug"),
    1.30     ("quiet", "verbose"),
    1.31 @@ -133,7 +130,13 @@
    1.32  
    1.33  fun unalias_raw_param (name, value) =
    1.34    case AList.lookup (op =) alias_params name of
    1.35 -    SOME name' => (name', value)
    1.36 +    SOME (name', []) => (name', value)
    1.37 +  | SOME (param' as (name', _)) =>
    1.38 +    if value <> ["false"] then
    1.39 +      param'
    1.40 +    else
    1.41 +      error ("Parameter " ^ quote name ^ " cannot be set to \"false\" \
    1.42 +             \(cf. " ^ quote name' ^ ").")
    1.43    | NONE =>
    1.44      case AList.lookup (op =) negated_alias_params name of
    1.45        SOME name' => (name', case value of
    1.46 @@ -340,7 +343,7 @@
    1.47        |> (if prover_name = default_minimize_prover then I else cons prover_name)
    1.48        |> space_implode ", "
    1.49    in
    1.50 -    sledgehammerN ^ " " ^ minN ^
    1.51 +    "sledgehammer" ^ " " ^ minN ^
    1.52      (if params = "" then "" else enclose " [" "]" params) ^
    1.53      " (" ^ space_implode " " fact_names ^ ")" ^
    1.54      (if i = 1 then "" else " " ^ string_of_int i)
    1.55 @@ -434,6 +437,6 @@
    1.56                       (minimize_command [] i) state
    1.57    end
    1.58  
    1.59 -val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer))
    1.60 +val setup = Try.register_tool ("sledgehammer", (40, auto, try_sledgehammer))
    1.61  
    1.62  end;