don't redo an axiom selection in the first round of Sledgehammer "minimize"!;
authorblanchet
Mon, 19 Apr 2010 19:41:15 +0200
changeset 36232 4d425766a47f
parent 36231 bede2d49ba3b
child 36233 1263bef003b3
don't redo an axiom selection in the first round of Sledgehammer "minimize"!; this is needlessly slow and messes up the declared functions/predicates in SPASS DFG files
src/HOL/Tools/ATP_Manager/atp_minimal.ML
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Apr 19 18:44:12 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Apr 19 19:41:15 2010 +0200
@@ -75,7 +75,8 @@
     val problem =
      {subgoal = subgoal, goal = (ctxt, (facts, goal)),
       relevance_override = {add = [], del = [], only = false},
-      axiom_clauses = SOME axclauses, filtered_clauses = filtered_clauses}
+      axiom_clauses = SOME axclauses,
+      filtered_clauses = SOME (the_default axclauses filtered_clauses)}
   in
     `outcome_of_result (prover params timeout problem)
     |>> tap (priority o string_of_outcome)