--- 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,