1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Mon May 21 11:31:52 2012 +0200
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Mon May 21 11:31:52 2012 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4    let
     1.5      val thy = Proof_Context.theory_of ctxt
     1.6      val prob_file = File.tmp_path (Path.explode "prob")
     1.7 -    val atp = case format of DFG _ => spass_newN | _ => eN
     1.8 +    val atp = case format of DFG _ => spassN | _ => eN
     1.9      val {exec, arguments, proof_delims, known_failures, ...} =
    1.10        get_atp thy atp ()
    1.11      val ord = effective_term_order ctxt atp

     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 21 11:31:52 2012 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon May 21 11:31:52 2012 +0200
     2.3 @@ -50,8 +50,6 @@
     2.4    val satallaxN : string
     2.5    val snarkN : string
     2.6    val spassN : string
     2.7 -  val spass_oldN : string
     2.8 -  val spass_newN : string
     2.9    val vampireN : string
    2.10    val waldmeisterN : string
    2.11    val z3_tptpN : string
    2.12 @@ -142,8 +140,6 @@
    2.13  val satallaxN = "satallax"
    2.14  val snarkN = "snark"
    2.15  val spassN = "spass"
    2.16 -val spass_oldN = "spass_old" (* for experiments *)
    2.17 -val spass_newN = "spass_new" (* for experiments *)
    2.18  val vampireN = "vampire"
    2.19  val waldmeisterN = "waldmeister"
    2.20  val z3_tptpN = "z3_tptp"
    2.21 @@ -370,7 +366,7 @@
    2.22     "required_vars" and "script/spass"). *)
    2.23  val spass_old_config : atp_config =
    2.24    {exec = (["ISABELLE_ATP"], "scripts/spass"),
    2.25 -   required_vars = [["SPASS_OLD_HOME", "SPASS_HOME"]],
    2.26 +   required_vars = [["SPASS_HOME"]],
    2.27     arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
    2.28       ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
    2.29        \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
    2.30 @@ -393,8 +389,6 @@
    2.31        (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), no_sosN)))]
    2.32       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)}
    2.33  
    2.34 -val spass_old = (spass_oldN, fn () => spass_old_config)
    2.35 -
    2.36  val spass_new_H1SOS = "-Heuristic=1 -SOS"
    2.37  val spass_new_H2 = "-Heuristic=2"
    2.38  val spass_new_H2SOS = "-Heuristic=2 -SOS"
    2.39 @@ -422,8 +416,6 @@
    2.40        (0.1000, (false, ((300, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2SOS))),
    2.41        (0.1000, (false, ((100, DFG DFG_Sorted, "mono_native", combs_and_liftingN, true), spass_new_H2NuVS0)))]}
    2.42  
    2.43 -val spass_new = (spass_newN, fn () => spass_new_config)
    2.44 -
    2.45  val spass =
    2.46    (spassN, fn () => if is_new_spass_version () then spass_new_config
    2.47                      else spass_old_config)
    2.48 @@ -649,8 +641,7 @@
    2.49  fun effective_term_order ctxt atp =
    2.50    let val ord = Config.get ctxt term_order in
    2.51      if ord = smartN then
    2.52 -      if atp = spass_newN orelse
    2.53 -         (atp = spassN andalso is_new_spass_version ()) then
    2.54 +      if atp = spassN andalso is_new_spass_version () then
    2.55          {is_lpo = false, gen_weights = true, gen_prec = true, gen_simp = false}
    2.56        else
    2.57          {is_lpo = false, gen_weights = false, gen_prec = false,
    2.58 @@ -665,10 +656,10 @@
    2.59    end
    2.60  
    2.61  val atps=
    2.62 -  [alt_ergo, e, leo2, dummy_thf, satallax, spass_old, spass_new, spass,
    2.63 -   vampire, z3_tptp, remote_e, remote_e_sine, remote_e_tofof, remote_iprover,
    2.64 -   remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire,
    2.65 -   remote_z3_tptp, remote_snark, remote_waldmeister]
    2.66 +  [alt_ergo, e, leo2, dummy_thf, satallax, spass, vampire, z3_tptp, remote_e,
    2.67 +   remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq,
    2.68 +   remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark,
    2.69 +   remote_waldmeister]
    2.70  
    2.71  val setup = fold add_atp atps
    2.72