# HG changeset patch
# User desharna
# Date 1639432382 -3600
# Node ID 482021527d1d4364cce6d9118fe1d120a56be872
# Parent  e83e92c0bcbd65079a838a15cf3ae2d4132c7431
tuned ATP to use fold_index

diff -r e83e92c0bcbd -r 482021527d1d src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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