tuned;

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

--- a/src/Pure/more_pattern.ML	Mon Dec 11 12:45:16 2023 +0100
+++ b/src/Pure/more_pattern.ML	Mon Dec 11 13:03:10 2023 +0100
@@ -39,7 +39,7 @@
 (* rewriting -- simple but fast *)
 
 fun match_rew thy tm (tm1, tm2) =
-  let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
+  let val rtm = perhaps (Term.rename_abs tm1 tm) tm2 in
     SOME (Envir.subst_term (Pattern.match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
       handle Pattern.MATCH => NONE
   end;