merged

--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Apr 17 14:56:38 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Apr 17 15:25:43 2012 +0200
@@ -109,7 +109,7 @@
     "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^
     " "
 
-fun string_for_failure Unprovable = "The problem is unprovable."
+fun string_for_failure Unprovable = "The generated problem is unprovable."
   | string_for_failure GaveUp = "The prover gave up."
   | string_for_failure ProofMissing =
     "The prover claims the conjecture is a theorem but did not provide a proof."
@@ -128,7 +128,7 @@
   | string_for_failure CantConnect = "Cannot connect to remote server."
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure Inappropriate =
-    "The problem lies outside the prover's scope."
+    "The generated problem lies outside the prover's scope."
   | string_for_failure OutOfResources = "The prover ran out of resources."
   | string_for_failure NoPerl = "Perl" ^ missing_message_tail
   | string_for_failure NoLibwwwPerl =

--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Apr 17 14:56:38 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Apr 17 15:25:43 2012 +0200
@@ -253,9 +253,8 @@
     (* supplied by Stephan Schulz *)
     "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
     \--destructive-er-aggressive --destructive-er --presat-simplify \
-    \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
-    \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
-    \-H'(4*" ^
+    \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
+    \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^
     e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^
     "(SimulateSOS, " ^
     (e_selection_heuristic_case heuristic
@@ -287,6 +286,8 @@
 fun effective_e_selection_heuristic ctxt =
   if is_new_e_version () then Config.get ctxt e_selection_heuristic else e_autoN
 
+fun e_kbo () = if is_new_e_version () then "KBO6" else "KBO"
+
 val e_config : atp_config =
   {exec = (["E_HOME"], "eproof"),
    required_vars = [],
@@ -296,7 +297,7 @@
         "--tstp-in --tstp-out --output-level=5 --silent " ^
         e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
         e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
-        "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
+        "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
         "--cpu-limit=" ^ string_of_int (to_secs 2 timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
@@ -638,6 +639,7 @@
   remote_atp waldmeisterN "Waldmeister" ["710"]
       [("#START OF PROOF", "Proved Goals:")]
       [(OutOfResources, "Too many function symbols"),
+       (Inappropriate, "****  Unexpected end of file."),
        (Crashed, "Unrecoverable Segmentation Fault")]
       Hypothesis Hypothesis
       (K ((50, CNF_UEQ, "mono_tags??", combsN, false), "") (* FUDGE *))