1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Dec 01 13:34:12 2011 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Dec 01 13:34:13 2011 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  val keepK = "keep"
     1.5  val type_encK = "type_enc"
     1.6  val soundK = "sound"
     1.7 -val slicingK = "slicing"
     1.8 +val sliceK = "slice"
     1.9  val lam_transK = "lam_trans"
    1.10  val e_weight_methodK = "e_weight_method"
    1.11  val force_sosK = "force_sos"
    1.12 @@ -361,7 +361,7 @@
    1.13    SH_FAIL of int * int |
    1.14    SH_ERROR
    1.15  
    1.16 -fun run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
    1.17 +fun run_sh prover_name prover type_enc sound max_relevant slice lam_trans
    1.18          e_weight_method force_sos hard_timeout timeout dir pos st =
    1.19    let
    1.20      val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
    1.21 @@ -381,7 +381,7 @@
    1.22                         e_weight_method |> the_default I)
    1.23                   #> (Option.map (Config.put ATP_Systems.force_sos)
    1.24                         force_sos |> the_default I))
    1.25 -    val params as {relevance_thresholds, max_relevant, slicing, ...} =
    1.26 +    val params as {relevance_thresholds, max_relevant, slice, ...} =
    1.27        Sledgehammer_Isar.default_params ctxt
    1.28            [("verbose", "true"),
    1.29             ("type_enc", type_enc),
    1.30 @@ -389,11 +389,11 @@
    1.31             ("lam_trans", lam_trans |> the_default "smart"),
    1.32             ("preplay_timeout", preplay_timeout),
    1.33             ("max_relevant", max_relevant),
    1.34 -           ("slicing", slicing),
    1.35 +           ("slice", slice),
    1.36             ("timeout", string_of_int timeout),
    1.37             ("preplay_timeout", preplay_timeout)]
    1.38      val default_max_relevant =
    1.39 -      Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
    1.40 +      Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice
    1.41          prover_name
    1.42      val is_appropriate_prop =
    1.43        Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name
    1.44 @@ -469,7 +469,7 @@
    1.45      val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
    1.46      val sound = AList.lookup (op =) args soundK |> the_default "false"
    1.47      val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
    1.48 -    val slicing = AList.lookup (op =) args slicingK |> the_default "true"
    1.49 +    val slice = AList.lookup (op =) args sliceK |> the_default "true"
    1.50      val lam_trans = AList.lookup (op =) args lam_transK
    1.51      val e_weight_method = AList.lookup (op =) args e_weight_methodK
    1.52      val force_sos = AList.lookup (op =) args force_sosK
    1.53 @@ -480,7 +480,7 @@
    1.54         minimizer has a chance to do its magic *)
    1.55      val hard_timeout = SOME (2 * timeout)
    1.56      val (msg, result) =
    1.57 -      run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
    1.58 +      run_sh prover_name prover type_enc sound max_relevant slice lam_trans
    1.59          e_weight_method force_sos hard_timeout timeout dir pos st
    1.60    in
    1.61      case result of
    1.62 @@ -555,7 +555,7 @@
    1.63     ("max_relevant", "0"),
    1.64     ("type_enc", type_enc),
    1.65     ("sound", "true"),
    1.66 -   ("slicing", "false"),
    1.67 +   ("slice", "false"),
    1.68     ("timeout", timeout |> Time.toSeconds |> string_of_int)]
    1.69  
    1.70  fun run_reconstructor trivial full m name reconstructor named_thms id