# HG changeset patch
# User blanchet
# Date 1271664902 -7200
# Node ID 16670b4f0baaed109ed5d01a6dae1d447575d5df
# Parent  0e4a01f3e7d3210c3577246e37038f29c4d6fd1c
set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format

diff -r 0e4a01f3e7d3 -r 16670b4f0baa src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Apr 19 09:53:31 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Apr 19 10:15:02 2010 +0200
@@ -240,10 +240,12 @@
 
 fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
 
+(* The "-VarWeight=3" option helps the higher-order problems, probably by
+   counteracting the presence of "hAPP". *)
 val spass_config : prover_config =
  {command = Path.explode "$SPASS_HOME/SPASS",
   arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
-    " -FullRed=0 -DocProof -TimeLimit=" ^
+    " -FullRed=0 -DocProof -VarWeight=3 -TimeLimit=" ^
     string_of_int (generous_to_secs timeout)),
   failure_strs =
     ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
diff -r 0e4a01f3e7d3 -r 16670b4f0baa src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 09:53:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Mon Apr 19 10:15:02 2010 +0200
@@ -514,7 +514,10 @@
 
 fun write_dfg_file debug full_types file clauses =
   let
-    val pool = empty_name_pool debug
+    (* Some of the helper functions below are not name-pool-aware. However,
+       there's no point in adding name pool support if the DFG format is on its
+       way out anyway. *)
+    val pool = NONE
     val (conjectures, axclauses, _, helper_clauses,
       classrel_clauses, arity_clauses) = clauses
     val (cma, cnh) = count_constants clauses
@@ -544,8 +547,6 @@
         tfree_clss @
         conjecture_clss @
         ["end_of_list.\n\n",
-        (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
-         "list_of_settings(SPASS).\n{*\nset_flag(VarWeight, 3).\n*}\nend_of_list.\n\n",
          "end_problem.\n"])
 
   in