# HG changeset patch
# User blanchet
# Date 1271698875 -7200
# Node ID 4d425766a47f27601feb4dda2d15a97f45f02436
# Parent  bede2d49ba3b2ddb6dd5a753cbbb2edaabf80c1a
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

diff -r bede2d49ba3b -r 4d425766a47f 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)