--- 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
--- 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) =>
--- 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)