author | desharna |
Mon, 13 Dec 2021 22:53:02 +0100 | |
changeset 74928 | 482021527d1d |
parent 74927 | e83e92c0bcbd |
child 74929 | a292605f12ef |
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Dec 10 16:46:29 2021 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Dec 13 22:53:02 2021 +0100 @@ -2939,8 +2939,7 @@ fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j / Real.fromInt num_facts in - map_index (apfst weight_of) facts - |> fold (uncurry add_line_weights) + fold_index (fn (i, fact) => add_line_weights (weight_of i) fact) facts end val get = these o AList.lookup (op =) problem in