choose facts to reprove more randomly, to avoid getting stuck with impossible problems at first

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Oct 17 02:22:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Oct 17 02:29:49 2013 +0200
@@ -1188,7 +1188,7 @@
                      Isar_Proof => 0
                    | Automatic_Proof => 2 * max_isar
                    | Isar_Proof_wegen_Prover_Flop => max_isar)
-                - 500 * length (isar_dependencies_of name_tabs th)
+                - 100 * length (isar_dependencies_of name_tabs th)
               val old_facts =
                 facts |> filter is_in_access_G
                       |> map (`priority_of)