made SML/NJ happier
authorblanchet
Sat, 19 Jul 2014 11:20:09 +0200
changeset 57574 e4ddd52e1b96
parent 57573 2bfbeb0e69cd
child 57575 b0d31645f47a
made SML/NJ happier
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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))