1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jun 08 08:47:43 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jun 08 08:47:43 2011 +0200
     1.3 @@ -96,7 +96,6 @@
     1.4     ("max_relevant", "smart"),
     1.5     ("max_mono_iters", "3"),
     1.6     ("max_new_mono_instances", "400"),
     1.7 -   ("explicit_apply", "smart"),
     1.8     ("isar_proof", "false"),
     1.9     ("isar_shrink_factor", "1"),
    1.10     ("slicing", "true"),
    1.11 @@ -112,14 +111,13 @@
    1.12     ("no_overlord", "overlord"),
    1.13     ("non_blocking", "blocking"),
    1.14     ("partial_types", "full_types"),
    1.15 -   ("implicit_apply", "explicit_apply"),
    1.16     ("no_isar_proof", "isar_proof"),
    1.17     ("no_slicing", "slicing")]
    1.18  
    1.19  val params_for_minimize =
    1.20    ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
    1.21 -   "max_new_mono_instances", "explicit_apply", "isar_proof",
    1.22 -   "isar_shrink_factor", "timeout", "preplay_timeout"]
    1.23 +   "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
    1.24 +   "preplay_timeout"]
    1.25  
    1.26  val property_dependent_params = ["provers", "full_types", "timeout"]
    1.27  
    1.28 @@ -284,7 +282,6 @@
    1.29      val max_relevant = lookup_option lookup_int "max_relevant"
    1.30      val max_mono_iters = lookup_int "max_mono_iters"
    1.31      val max_new_mono_instances = lookup_int "max_new_mono_instances"
    1.32 -    val explicit_apply = lookup_option lookup_bool "explicit_apply"
    1.33      val isar_proof = lookup_bool "isar_proof"
    1.34      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    1.35      val slicing = mode <> Auto_Try andalso lookup_bool "slicing"
    1.36 @@ -299,9 +296,9 @@
    1.37       provers = provers, relevance_thresholds = relevance_thresholds,
    1.38       max_relevant = max_relevant, max_mono_iters = max_mono_iters,
    1.39       max_new_mono_instances = max_new_mono_instances, type_sys = type_sys,
    1.40 -     explicit_apply = explicit_apply, isar_proof = isar_proof,
    1.41 -     isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    1.42 -     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    1.43 +     isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
    1.44 +     slicing = slicing, timeout = timeout, preplay_timeout = preplay_timeout,
    1.45 +     expect = expect}
    1.46    end
    1.47  
    1.48  fun get_params mode ctxt = extract_params mode (default_raw_params ctxt)