1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Dec 20 23:36:58 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Dec 21 01:12:17 2010 +0100
     1.3 @@ -125,7 +125,8 @@
     1.4    | string_for_failure prover (UnknownError string) =
     1.5      (* "An" is correct for "ATP" and "SMT". *)
     1.6      "An " ^ prover ^ " error occurred" ^
     1.7 -    (if string = "" then "." else ":\n" ^ string)
     1.8 +    (if string = "" then ". (Pass the \"verbose\" option for details.)"
     1.9 +     else ":\n" ^ string)
    1.10  
    1.11  fun extract_delimited (begin_delim, end_delim) output =
    1.12    output |> first_field begin_delim |> the |> snd

     2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Dec 20 23:36:58 2010 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Dec 21 01:12:17 2010 +0100
     2.3 @@ -90,21 +90,18 @@
     2.4     account for the overhead of the script itself, which is in fact much
     2.5     lower. *)
     2.6  fun e_bonus () =
     2.7 -  case getenv "E_VERSION" of
     2.8 -    "" => 2000
     2.9 -  | version =>
    2.10 -    if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 2000
    2.11 -    else 1000
    2.12 +  if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000
    2.13  
    2.14  val tstp_proof_delims =
    2.15    ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
    2.16  
    2.17 -val e_generate_weights = Unsynchronized.ref false
    2.18 -val e_weight_factor = Unsynchronized.ref 60.0
    2.19 +val e_generate_weights = Unsynchronized.ref true
    2.20 +val e_weight_factor = Unsynchronized.ref 40.0
    2.21  val e_default_weight = Unsynchronized.ref 0.5
    2.22  
    2.23  fun e_weights weights =
    2.24 -  if !e_generate_weights then
    2.25 +  if !e_generate_weights andalso
    2.26 +     string_ord (getenv "E_VERSION", "1.2B") <> LESS then
    2.27      "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
    2.28      \--destructive-er-aggressive --destructive-er --presat-simplify \
    2.29      \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \