diff -r 702278df3b57 -r 960a3429615c src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Dec 07 23:14:39 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Dec 08 00:48:50 2012 +0100
@@ -593,9 +593,9 @@
     |> exists (exists_Const is_exists) ts ? cons skos_feature
   end
 
-(* Too many dependencies is a sign that a crazy decision procedure is at work.
-   There isn't much to learn from such proofs. *)
-val max_dependencies = 10
+(* Too many dependencies is a sign that a decision procedure is at work. There
+   isn't much to learn from such proofs. *)
+val max_dependencies = 20
 val atp_dependency_default_max_facts = 50
 
 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)