1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4     ("isar_proof", "false"),
     1.5     ("isar_shrink_factor", "1"),
     1.6     ("slicing", "true"),
     1.7 -   ("metis_timeout", "5")]
     1.8 +   ("preplay_timeout", "5")]
     1.9  
    1.10  val alias_params =
    1.11    [("prover", "provers"),
    1.12 @@ -107,7 +107,7 @@
    1.13  val params_for_minimize =
    1.14    ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
    1.15     "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
    1.16 -   "metis_timeout"]
    1.17 +   "preplay_timeout"]
    1.18  
    1.19  val property_dependent_params = ["provers", "full_types", "timeout"]
    1.20  
    1.21 @@ -277,8 +277,9 @@
    1.22      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    1.23      val slicing = not auto andalso lookup_bool "slicing"
    1.24      val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
    1.25 -    val metis_timeout =
    1.26 -      if auto then Time.zeroTime else lookup_time "metis_timeout" |> the_timeout
    1.27 +    val preplay_timeout =
    1.28 +      if auto then Time.zeroTime
    1.29 +      else lookup_time "preplay_timeout" |> the_timeout
    1.30      val expect = lookup_string "expect"
    1.31    in
    1.32      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    1.33 @@ -287,7 +288,7 @@
    1.34       max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
    1.35       explicit_apply = explicit_apply, isar_proof = isar_proof,
    1.36       isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    1.37 -     timeout = timeout, metis_timeout = metis_timeout, expect = expect}
    1.38 +     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    1.39    end
    1.40  
    1.41  fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)