src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

 (*** Isabelle-agnostic machine learning ***)
 
 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))
     end)