tuned ATP to use fold_index
authordesharna
Mon, 13 Dec 2021 22:53:02 +0100
changeset 74928 482021527d1d
parent 74927 e83e92c0bcbd
child 74929 a292605f12ef
tuned ATP to use fold_index
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