author | blanchet |
Sat, 19 Jul 2014 11:20:09 +0200 | |
changeset 57574 | e4ddd52e1b96 |
parent 57573 | 2bfbeb0e69cd |
child 57575 | b0d31645f47a |
--- 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))