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