# HG changeset patch
# User blanchet
# Date 1381299173 -7200
# Node ID 824db6ab33391ec2c80554bc1798a186826e43e6
# Parent  fcb7bbbe379992ea7bf5817093b50d2f924446a2
crank up limit a bit -- truly huge background theories are still nearly 3 times larger

diff -r fcb7bbbe3799 -r 824db6ab3339 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 22:33:05 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 09 08:12:53 2013 +0200
@@ -61,7 +61,7 @@
 val max_facts_for_duplicates = 50000
 val max_facts_for_duplicate_matching = 25000
 val max_facts_for_complex_check = 25000
-val max_simps_for_clasimpset = 5000
+val max_simps_for_clasimpset = 10000
 
 (* experimental feature *)
 val instantiate_inducts =