1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 09 17:33:17 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 09 17:33:17 2011 +0200
     1.3 @@ -13,8 +13,7 @@
     1.4  val slicingK = "slicing"
     1.5  val lambda_translationK = "lambda_translation"
     1.6  val e_weight_methodK = "e_weight_method"
     1.7 -val spass_force_sosK = "spass_force_sos"
     1.8 -val vampire_force_sosK = "vampire_force_sos"
     1.9 +val force_sosK = "force_sos"
    1.10  val max_relevantK = "max_relevant"
    1.11  val minimizeK = "minimize"
    1.12  val minimize_timeoutK = "minimize_timeout"
    1.13 @@ -354,8 +353,8 @@
    1.14    SH_ERROR
    1.15  
    1.16  fun run_sh prover_name prover type_enc sound max_relevant slicing
    1.17 -        lambda_translation e_weight_method spass_force_sos vampire_force_sos
    1.18 -        hard_timeout timeout dir pos st =
    1.19 +        lambda_translation e_weight_method force_sos hard_timeout timeout dir
    1.20 +        pos st =
    1.21    let
    1.22      val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
    1.23      val i = 1
    1.24 @@ -375,10 +374,8 @@
    1.25                         lambda_translation |> the_default I)
    1.26                   #> (Option.map (Config.put ATP_Systems.e_weight_method)
    1.27                         e_weight_method |> the_default I)
    1.28 -                 #> (Option.map (Config.put ATP_Systems.spass_force_sos)
    1.29 -                       spass_force_sos |> the_default I)
    1.30 -                 #> (Option.map (Config.put ATP_Systems.vampire_force_sos)
    1.31 -                       vampire_force_sos |> the_default I)
    1.32 +                 #> (Option.map (Config.put ATP_Systems.force_sos)
    1.33 +                       force_sos |> the_default I)
    1.34                   #> Config.put Sledgehammer_Provers.measure_run_time true)
    1.35      val params as {relevance_thresholds, max_relevant, slicing, ...} =
    1.36        Sledgehammer_Isar.default_params ctxt
    1.37 @@ -466,9 +463,7 @@
    1.38      val slicing = AList.lookup (op =) args slicingK |> the_default "true"
    1.39      val lambda_translation = AList.lookup (op =) args lambda_translationK
    1.40      val e_weight_method = AList.lookup (op =) args e_weight_methodK
    1.41 -    val spass_force_sos = AList.lookup (op =) args spass_force_sosK
    1.42 -      |> Option.map (curry (op <>) "false")
    1.43 -    val vampire_force_sos = AList.lookup (op =) args vampire_force_sosK
    1.44 +    val force_sos = AList.lookup (op =) args force_sosK
    1.45        |> Option.map (curry (op <>) "false")
    1.46      val dir = AList.lookup (op =) args keepK
    1.47      val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
    1.48 @@ -477,8 +472,8 @@
    1.49      val hard_timeout = SOME (2 * timeout)
    1.50      val (msg, result) =
    1.51        run_sh prover_name prover type_enc sound max_relevant slicing
    1.52 -        lambda_translation e_weight_method spass_force_sos vampire_force_sos
    1.53 -        hard_timeout timeout dir pos st
    1.54 +        lambda_translation e_weight_method force_sos hard_timeout timeout dir
    1.55 +        pos st
    1.56    in
    1.57      case result of
    1.58        SH_OK (time_isa, time_prover, names) =>