# HG changeset patch
# User desharna
# Date 1639122782 -3600
# Node ID cab76af373e767890e66752dcc8a12fe1aad0387
# Parent  d969474ddc459fa142c651caee5060e7249bf2a1
tuned metis to use map_index

diff -r d969474ddc45 -r cab76af373e7 src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Fri Dec 10 08:58:09 2021 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Fri Dec 10 08:53:02 2021 +0100
@@ -206,12 +206,9 @@
         |> Monomorph.monomorph atp_schematic_consts_of ctxt
         |> chop (length conj_clauses)
         |> apply2 (maps (map (zero_var_indexes o snd)))
-    val num_conjs = length conj_clauses
     (* Pretend every clause is a "simp" rule, to guide the term ordering. *)
     val clauses =
-      map2 (fn j => pair (Int.toString j, (Local, Simp))) (0 upto num_conjs - 1) conj_clauses @
-      map2 (fn j => pair (Int.toString (num_conjs + j), (Local, Simp)))
-        (0 upto length fact_clauses - 1) fact_clauses
+      map_index (apfst (fn j => (Int.toString j, (Local, Simp)))) (conj_clauses @ fact_clauses)
     val (old_skolems, props) =
       fold_rev (fn (name, th) => fn (old_skolems, props) =>
            th |> Thm.prop_of |> Logic.strip_imp_concl
diff -r d969474ddc45 -r cab76af373e7 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Dec 10 08:58:09 2021 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Dec 10 08:53:02 2021 +0100
@@ -682,10 +682,10 @@
           SOME ((ax_no, cluster_no),
             clusters_in_term true t |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
         | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]))
-
       val prems = Logic.strip_imp_prems (Thm.prop_of prems_imp_false)
-      val substs = prems |> map2 subst_info_of_prem (1 upto length prems)
-                         |> sort (int_ord o apply2 fst)
+      val substs =
+        map_index (fn (i, prem) => subst_info_of_prem (i + 1) prem) prems
+        |> sort (int_ord o apply2 fst)
       val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs
       val clusters = maps (op ::) depss
       val ordered_clusters =
@@ -702,7 +702,7 @@
                                                   (Integer.add 1)) substs
         |> Int_Tysubst_Table.dest
       val needed_axiom_props =
-        0 upto length axioms - 1 ~~ axioms
+        map_index I axioms
         |> map_filter (fn (_, NONE) => NONE
                         | (ax_no, SOME (_, t)) =>
                           if exists (fn ((ax_no', _), n) =>
diff -r d969474ddc45 -r cab76af373e7 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Fri Dec 10 08:58:09 2021 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Fri Dec 10 08:53:02 2021 +0100
@@ -151,14 +151,14 @@
     val new_skolem = Config.get ctxt new_skolem orelse null (Meson.choice_theorems thy)
     val do_lams = lam_trans = liftingN ? introduce_lam_wrappers ctxt
     val th_cls_pairs =
-      map2 (fn j => fn th =>
+      map_index (fn (j, th) =>
         (Thm.get_name_hint th,
           th
           |> Drule.eta_contraction_rule
           |> Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt new_skolem
                (lam_trans = combsN) j
           ||> map do_lams))
-        (0 upto length ths0 - 1) ths0
+        ths0
     val ths = maps (snd o snd) th_cls_pairs
     val dischargers = map (fst o snd) th_cls_pairs
     val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)