--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Dec 10 14:20:27 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Dec 10 16:46:29 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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Dec 10 14:20:27 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Dec 10 16:46:29 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 =