1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Dec 01 13:34:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Dec 01 13:34:13 2011 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4     ("max_new_mono_instances", "200"),
     1.5     ("isar_proof", "false"),
     1.6     ("isar_shrink_factor", "1"),
     1.7 -   ("slicing", "true"),
     1.8 +   ("slice", "true"),
     1.9     ("preplay_timeout", "4")]
    1.10  
    1.11  val alias_params =
    1.12 @@ -107,7 +107,7 @@
    1.13     ("non_blocking", "blocking"),
    1.14     ("unsound", "sound"),
    1.15     ("no_isar_proof", "isar_proof"),
    1.16 -   ("no_slicing", "slicing")]
    1.17 +   ("dont_slice", "slice")]
    1.18  
    1.19  val params_for_minimize =
    1.20    ["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans",
    1.21 @@ -289,7 +289,7 @@
    1.22      val max_new_mono_instances = lookup_int "max_new_mono_instances"
    1.23      val isar_proof = lookup_bool "isar_proof"
    1.24      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    1.25 -    val slicing = mode <> Auto_Try andalso lookup_bool "slicing"
    1.26 +    val slice = mode <> Auto_Try andalso lookup_bool "slice"
    1.27      val timeout =
    1.28        (if mode = Auto_Try then NONE else lookup_time "timeout") |> the_timeout
    1.29      val preplay_timeout =
    1.30 @@ -302,8 +302,8 @@
    1.31       lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
    1.32       max_relevant = max_relevant, max_mono_iters = max_mono_iters,
    1.33       max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
    1.34 -     isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    1.35 -     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    1.36 +     isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout,
    1.37 +     preplay_timeout = preplay_timeout, expect = expect}
    1.38    end
    1.39  
    1.40  fun get_params mode = extract_params mode o default_raw_params