# HG changeset patch
# User blanchet
# Date 1289149404 -3600
# Node ID 391c9256265cc3c4d1af7f6ede8ca01343c7f315
# Parent  1d3df64b1f88bf6cfdf836386f27dffef0321709
don't pass too many facts on the first iteration of the SMT solver

diff -r 1d3df64b1f88 -r 391c9256265c src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Nov 07 18:02:02 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Nov 07 18:03:24 2010 +0100
@@ -104,7 +104,7 @@
     else is_atp_installed thy name
   end
 
-val smt_default_max_relevant = 300 (* FUDGE (FIXME) *)
+val smt_default_max_relevant = 250 (* FUDGE (FIXME) *)
 val auto_max_relevant_divisor = 2 (* FUDGE *)
 
 fun default_max_relevant_for_prover thy name =