# HG changeset patch
# User blanchet
# Date 1354789510 -3600
# Node ID d84a5ab736bb23399cd3be049ce0c8961569b9c4
# Parent  5c9a2f5ab3239893c5d9fc8d9646e14c85e94658
reduce max number of dependencies for MaSh to get rid of junk

diff -r 5c9a2f5ab323 -r d84a5ab736bb src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
@@ -590,7 +590,7 @@
 
 (* 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 = 100
+val max_dependencies = 10
 val atp_dependency_default_max_facts = 50
 
 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
@@ -747,8 +747,7 @@
             in
               (fact_G, mash_QUERY ctxt overlord max_facts (parents, feats))
             end)
-    val (chained, unchained) =
-      List.partition (fn ((_, (scope, _)), _) => scope = Chained) facts
+    val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
     val raw_mash =
       facts |> suggested_facts suggs
             (* The weights currently returned by "mash.py" are too spaced out to