# HG changeset patch
# User wenzelm
# Date 1702296190 -3600
# Node ID b0774e7d19496aa65f5e1c93b02deefc32c2f6d9
# Parent  a49bdb686545a2bee507d6941b08f6656039d5a7
tuned;

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;
diff -r a49bdb686545 -r b0774e7d1949 src/Pure/more_pattern.ML
--- 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;