src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 57574 e4ddd52e1b96
parent 57561 8200e1eb367f
child 57658 f55c173a3cbc
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 18 22:16:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jul 19 11:20:09 2014 +0200
@@ -278,7 +278,7 @@
 structure MaSh =
 struct
 
-fun select_visible_facts big_number recommends =
+fun select_visible_facts (big_number : real) recommends =
   List.app (fn at =>
     let val (j, ov) = Array.sub (recommends, at) in
       Array.update (recommends, at, (j, big_number + ov))