# HG changeset patch
# User desharna
# Date 1682587073 -7200
# Node ID ce09ea4c0f931e60458a70aa614890286fb2471d
# Parent  5aae99b191ebdc6741bddd8dae30e17f573c3761
tuned; avoided intermediate list

diff -r 5aae99b191eb -r ce09ea4c0f93 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Apr 26 22:02:59 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Apr 27 11:17:53 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')