--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jul 27 12:01:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Tue Jul 27 13:15:58 2010 +0200
@@ -171,6 +171,7 @@
val axiom_prefix = "ax_"
val conjecture_prefix = "conj_"
val arity_clause_prefix = "clsarity_"
+val tfrees_name = "tfrees"
fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
@@ -255,7 +256,7 @@
map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
fun problem_line_for_free_type lit =
- Fof ("tfree_tcs", Conjecture, formula_for_fo_literal lit)
+ Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
fun problem_lines_for_free_types conjectures =
let
val litss = map free_type_literals_for_conjecture conjectures
@@ -404,6 +405,8 @@
val conjecture_lines =
map (problem_line_for_conjecture full_types) conjectures
val tfree_lines = problem_lines_for_free_types conjectures
+ (* Reordering these might or might not confuse the proof reconstruction
+ code or the SPASS Flotter hack. *)
val problem =
[("Relevant facts", axiom_lines),
("Class relationships", class_rel_lines),