# HG changeset patch
# User blanchet
# Date 1334663671 -7200
# Node ID e33d957ae2bf574ec9602c8c7102589f8f2e5829
# Parent  cb44d09d9d22748f2f87c51506855e0361dfb78b
avoid option introduced in E 1.2 when invoking older versions of E

diff -r cb44d09d9d22 -r e33d957ae2bf src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Apr 17 11:03:08 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Apr 17 13:54:31 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 =