merged

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Apr 27 16:15:19 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Apr 27 17:06:03 2023 +0200
@@ -956,14 +956,14 @@
                 val (binder_Us, body_U) = strip_ty U
                 val in_U_vars = fold Term.add_tvarsT binder_Us []
                 val out_U_vars = Term.add_tvarsT body_U []
-                fun filt (U_var, T) =
+                fun filt U_var T =
                   if keep (member (op =) in_U_vars U_var,
                            member (op =) out_U_vars U_var) then
                     T
                   else
                     dummyT
                 val U_args = (s, U) |> robust_const_type_args thy
-              in map (filt o apfst dest_TVar) (U_args ~~ T_args) end
+              in map2 (fn U_arg => filt (dest_TVar U_arg)) U_args T_args end
               handle TYPE _ => T_args
           fun is_always_ctr (s', T') =
             s' = s andalso type_equiv thy (T', robust_const_type thy s')

--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Apr 27 16:15:19 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Apr 27 17:06:03 2023 +0200
@@ -438,10 +438,9 @@
 
 fun is_same_formula comm subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) =
     q1 = q2 andalso length xs1 = length xs2 andalso
-    is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2
+    is_same_formula comm (map2 (fn (x1, _) => fn (x2, _) => (x1, x2)) xs1 xs2 @ subst) phi1 phi2
   | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) =
-    c1 = c2 andalso length phis1 = length phis2 andalso
-    forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2)
+    c1 = c2 andalso forall2 (is_same_formula comm subst) phis1 phis2
   | is_same_formula comm subst (AAtom (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) =
     is_same_term subst tm1 tm2 orelse
     (comm andalso is_same_term subst (ATerm (("equal", tys), [tm12, tm11])) tm2)

--- a/src/HOL/Tools/ATP/atp_util.ML	Thu Apr 27 16:15:19 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Apr 27 17:06:03 2023 +0200
@@ -50,11 +50,16 @@
   val short_thm_name : Proof.context -> thm -> string
   val map_prod : ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd
   val compare_length_with : 'a list -> int -> order
+  val forall2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
 end;
 
 structure ATP_Util : ATP_UTIL =
 struct
 
+fun forall2 _ [] [] = true
+  | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
+  | forall2 _ _ _ = false
+
 fun timestamp_format time =
   Date.fmt "%Y-%m-%d %H:%M:%S." (Date.fromTimeLocal time) ^
   (StringCvt.padLeft #"0" 3 (string_of_int (Time.toMilliseconds time - 1000 * Time.toSeconds time)))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Apr 27 16:15:19 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Apr 27 17:06:03 2023 +0200
@@ -322,7 +322,7 @@
         val (new_names, ctxt') = Variable.variant_fixes new_names0 ctxt
         val ys = map2 pair new_names Ts
       in
-        (ys, ((map Free xs ~~ map Free ys) @ subst, ctxt'))
+        (ys, (map2 (fn x => fn y => (Free x, Free y)) xs ys @ subst, ctxt'))
       end
 
     fun rationalize_step (Prove {qualifiers, obtains, label, goal, subproofs, facts, proof_methods,