# HG changeset patch
# User blanchet
# Date 1360916240 -3600
# Node ID fb16c4276620bc6ff3190a602068d2011fd89a9e
# Parent  f8dc1c94ef8bf34b3774b5994276d7de3b5dc2ce
tuning

diff -r f8dc1c94ef8b -r fb16c4276620 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Feb 14 23:54:46 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Feb 15 09:17:20 2013 +0100
@@ -636,7 +636,7 @@
    isn't much to learn from such proofs. *)
 val max_dependencies = 20
 
-val prover_dependency_default_max_facts = 50
+val prover_default_max_facts = 50
 
 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
 val typedef_dep = nickname_of_thm @{thm CollectI}
@@ -704,8 +704,8 @@
       val facts =
         facts
         |> mepo_suggested_facts ctxt params prover
-               (max_facts |> the_default prover_dependency_default_max_facts)
-               NONE hyp_ts concl_t
+               (max_facts |> the_default prover_default_max_facts) NONE hyp_ts
+               concl_t
         |> fold (add_isar_dep facts) isar_deps
         |> map nickify
     in