# 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