changeset 59172 | d1c500e0a722 |
parent 59058 | a78612c67ec0 |
child 59471 | ca459352d8c5 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Dec 21 22:49:40 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Dec 22 14:33:53 2014 +0100 @@ -1434,7 +1434,7 @@ val max_isar = 1000 * max_dependencies fun priority_of th = - random_range 0 max_isar + + Random.random_range 0 max_isar + (case try (Graph.get_node access_G) (nickname_of_thm th) of SOME (Isar_Proof, _, deps) => ~100 * length deps | SOME (Automatic_Proof, _, _) => 2 * max_isar