# HG changeset patch
# User wenzelm
# Date 1729722374 -7200
# Node ID 389f315f8c24ef08d5bf4603f6d8d4db7bb6cd58
# Parent  8205db6977dd503106bd99a796e5fd32873cec2c
tuned;

diff -r 8205db6977dd -r 389f315f8c24 src/Pure/more_pattern.ML
--- a/src/Pure/more_pattern.ML	Thu Oct 24 00:20:21 2024 +0200
+++ b/src/Pure/more_pattern.ML	Thu Oct 24 00:26:14 2024 +0200
@@ -54,7 +54,7 @@
 
 datatype mode = Bottom | Top | Yoyo;
 
-fun rewrite_term_mode mode thy rules procs term =
+fun rewrite_term_mode mode thy rules procs =
   let
     fun variant_absfree bounds x tm =
       let
@@ -130,10 +130,9 @@
           | NONE => NONE));
 
     fun rew_yoyo bounds skel = perhaps_loop (rew_yoyo2 bounds skel);
-
-
-    val rewrite = (case mode of Bottom => rew_bottom | Top => rew_top | Yoyo => rew_yoyo);
-  in the_default term (rewrite 0 skel0 term) end;
+  in
+    perhaps ((case mode of Bottom => rew_bottom | Top => rew_top | Yoyo => rew_yoyo) 0 skel0)
+  end;
 
 in