src/HOL/Tools/ATP/atp_problem_generate.ML
changeset 74928 482021527d1d
parent 74918 68a0f9a8561d
child 74949 90290869796f
--- 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