1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
     1.3 @@ -590,7 +590,7 @@
     1.4  
     1.5  (* Too many dependencies is a sign that a crazy decision procedure is at work.
     1.6     There isn't much to learn from such proofs. *)
     1.7 -val max_dependencies = 100
     1.8 +val max_dependencies = 10
     1.9  val atp_dependency_default_max_facts = 50
    1.10  
    1.11  (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
    1.12 @@ -747,8 +747,7 @@
    1.13              in
    1.14                (fact_G, mash_QUERY ctxt overlord max_facts (parents, feats))
    1.15              end)
    1.16 -    val (chained, unchained) =
    1.17 -      List.partition (fn ((_, (scope, _)), _) => scope = Chained) facts
    1.18 +    val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
    1.19      val raw_mash =
    1.20        facts |> suggested_facts suggs
    1.21              (* The weights currently returned by "mash.py" are too spaced out to