# HG changeset patch
# User wenzelm
# Date 1639512787 -3600
# Node ID d4d3dec0970ae12ca29d87895e54dc1f94cac1a8
# Parent  a292605f12efaf3e6da5bd7ef3ce3dc448b22596# Parent  f76bf7b5baed7859cbc1aefee06ca51f04a4ba68
merged

diff -r f76bf7b5baed -r d4d3dec0970a src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Dec 14 21:12:33 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Dec 14 21:13:07 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
diff -r f76bf7b5baed -r d4d3dec0970a src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Dec 14 21:12:33 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Dec 14 21:13:07 2021 +0100
@@ -195,8 +195,8 @@
 fun smooth_weight_of_fact rank = Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0 (* FUDGE *)
 fun steep_weight_of_fact rank = Math.pow (0.62, log2 (Real.fromInt (rank + 1))) (* FUDGE *)
 
-fun weight_facts_smoothly facts = facts ~~ map smooth_weight_of_fact (0 upto length facts - 1)
-fun weight_facts_steeply facts = facts ~~ map steep_weight_of_fact (0 upto length facts - 1)
+fun weight_facts_smoothly facts = map_index (swap o apfst smooth_weight_of_fact) facts
+fun weight_facts_steeply facts = map_index (swap o apfst steep_weight_of_fact) facts
 
 fun sort_array_suffix cmp needed a =
   let
diff -r f76bf7b5baed -r d4d3dec0970a src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Dec 14 21:12:33 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Dec 14 21:13:07 2021 +0100
@@ -99,8 +99,7 @@
   transform_elim_prop
   #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite)
 
-fun get_slices slice slices =
-  (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
+fun get_slices slice slices = map_index I slices |> not slice ? (List.last #> single)
 
 fun get_facts_of_filter _ [(_, facts)] = facts
   | get_facts_of_filter fact_filter factss =