1.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Mar 19 15:33:18 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Mar 19 16:04:15 2010 +0100
     1.3 @@ -184,7 +184,7 @@
     1.4    emit_structured_proof = full};
     1.5  
     1.6  val vampire = tptp_prover ("vampire", vampire_prover_config false);
     1.7 -val vampire_full = tptp_prover ("vampire_full", vampire_prover_config true);
     1.8 +val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true);
     1.9  
    1.10  
    1.11  (* E prover *)
    1.12 @@ -206,7 +206,7 @@
    1.13    emit_structured_proof = full};
    1.14  
    1.15  val eprover = tptp_prover ("e", eprover_config false);
    1.16 -val eprover_full = tptp_prover ("e_full", eprover_config true);
    1.17 +val eprover_isar = tptp_prover ("e_isar", eprover_config true);
    1.18  
    1.19  
    1.20  (* SPASS *)
    1.21 @@ -290,7 +290,7 @@
    1.22    "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const);
    1.23  
    1.24  val provers =
    1.25 -  [spass, vampire, eprover, vampire_full, eprover_full, spass_no_tc,
    1.26 +  [spass, vampire, eprover, vampire_isar, eprover_isar, spass_no_tc,
    1.27     remote_vampire, remote_spass, remote_eprover]
    1.28  val prover_setup = fold add_prover provers
    1.29