# HG changeset patch
# User blanchet
# Date 1280229358 -7200
# Node ID 7ff321103cd8321030c3c72f52927abdfd87f368
# Parent  f0a4aa17f23fbdbfbecafd512bd6f26fe20a2309
negate tfree conjecture

diff -r f0a4aa17f23f -r 7ff321103cd8 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
--- 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),