changeset 50438 | 9bb7868a4c20 |
parent 50435 | e8f2d7a3ef53 |
child 50440 | ca99c269ca3a |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Dec 08 00:48:50 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Dec 08 00:48:50 2012 +0100 @@ -451,7 +451,7 @@ in case find_index (curry fact_eq fact o fst) sels of ~1 => (case find_index (curry fact_eq fact) unks of - ~1 => score_at sel_len + ~1 => score_at (sel_len - 1) | _ => NONE) | rank => score_at rank end