diff -r a49bdb686545 -r b0774e7d1949 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Dec 11 12:45:16 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Mon Dec 11 13:03:10 2023 +0100
@@ -100,7 +100,7 @@
       in
         get_first (fn (_, (prems, (tm1, tm2))) =>
         let
-          fun ren t = the_default t (Term.rename_abs tm1 tm t);
+          fun ren t = perhaps (Term.rename_abs tm1 tm) t;
           val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
           val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
           val prems' = map (apply2 (Envir.subst_term env o inc o ren)) prems;