# HG changeset patch
# User blanchet
# Date 1381969789 -7200
# Node ID 18b23d787062a727a17295677119cf3d5c830083
# Parent  b4e6cd4cab92c1916fa4baeb0f467b6138add36d
choose facts to reprove more randomly, to avoid getting stuck with impossible problems at first

diff -r b4e6cd4cab92 -r 18b23d787062 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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)