--- 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
--- 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 =