src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
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