# HG changeset patch
# User blanchet
# Date 1280136407 -7200
# Node ID bb39190370fe86d3a4ca246ae82e3437936f2869
# Parent  7911e78a7122325f6b30fdedeca2ac2f9f27e160
generate close formulas for SPASS, but not for the others (to avoid clutter)

diff -r 7911e78a7122 -r bb39190370fe src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 11:21:25 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 11:26:47 2010 +0200
@@ -22,7 +22,7 @@
   val axiom_prefix : string
   val conjecture_prefix : string
   val write_tptp_file :
-    theory -> bool -> bool -> bool -> Path.T
+    theory -> bool -> bool -> bool -> bool -> Path.T
     -> fol_clause list * fol_clause list * fol_clause list * fol_clause list
        * class_rel_clause list * arity_clause list
     -> string Symtab.table * int
@@ -370,11 +370,10 @@
   repair_problem_with_const_table thy explicit_forall full_types
       (const_table_for_problem explicit_apply problem) problem
 
-fun write_tptp_file thy readable_names full_types explicit_apply file
-                    (conjectures, axiom_clauses, extra_clauses, helper_clauses,
-                     class_rel_clauses, arity_clauses) =
+fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
+                    file (conjectures, axiom_clauses, extra_clauses,
+                          helper_clauses, class_rel_clauses, arity_clauses) =
   let
-    val explicit_forall = true (* ### FIXME *)
     val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
     val class_rel_lines =
       map problem_line_for_class_rel_clause class_rel_clauses