# HG changeset patch
# User blanchet
# Date 1332265365 -3600
# Node ID 7585d0120f1dca8a35dd904f69844eeed6c19e2e
# Parent  e4ee21290dcae1f5a57dcfe68f2a1b209e3be4d2
tweaks

diff -r e4ee21290dca -r 7585d0120f1d src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 20 17:20:33 2012 +0000
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 20 18:42:45 2012 +0100
@@ -578,20 +578,20 @@
                    |> maybe_enclose "set_precedence(" ")."]
        else
          [])
-    fun list_of _ _ _ [] = []
-      | list_of heading bef aft ss =
-        "list_of_" ^ heading ^ ".\n" :: bef :: map (suffix "\n") ss @
-        [aft, "end_of_list.\n\n"]
+    fun list_of _ [] = []
+      | list_of heading ss =
+        "list_of_" ^ heading ^ ".\n" :: map (suffix "\n") ss @
+        ["end_of_list.\n\n"]
   in
     "\nbegin_problem(isabelle).\n\n" ::
-    list_of "descriptions" "" ""
+    list_of "descriptions"
             ["name({**}).", "author({**}).", "status(unknown).",
              "description({**})."] @
-    list_of "symbols" "" "" syms @
-    list_of "declarations" "" "" decls @
-    list_of "formulae(axioms)" "" "" axioms @
-    list_of "formulae(conjectures)" "" "" conjs @
-    list_of "settings(SPASS)" "{*\n" "*}\n" settings @
+    list_of "symbols" syms @
+    list_of "declarations" decls @
+    list_of "formulae(axioms)" axioms @
+    list_of "formulae(conjectures)" conjs @
+    list_of "settings(SPASS)" settings @
     ["end_problem.\n"]
   end
 
diff -r e4ee21290dca -r 7585d0120f1d src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 20 17:20:33 2012 +0000
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 20 18:42:45 2012 +0100
@@ -311,7 +311,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 "Auto") ^ " " ^
+        "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^
         "--cpu-limit=" ^ string_of_int (to_secs 2 timeout),
    proof_delims = tstp_proof_delims,
    known_failures =