# HG changeset patch
# User blanchet
# Date 1405761609 -7200
# Node ID e4ddd52e1b96d531b4efeffcdefe14b720c0ec7b
# Parent  2bfbeb0e69cd1a193ccca2e5ab0805dae75267f6
made SML/NJ happier

diff -r 2bfbeb0e69cd -r e4ddd52e1b96 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))