# HG changeset patch
# User desharna
# Date 1682589014 -7200
# Node ID 8734ca279e59a524fa244bbc4f7fed0f4a4ca10f
# Parent  55b81d14a1b884f6cc15e357f923e0df222244ab
tuned; avoided intermediate lists

diff -r 55b81d14a1b8 -r 8734ca279e59 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Apr 27 11:46:58 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Apr 27 11:50:14 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,