diff -r 46591222e4fc -r e55d712eff7b src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Isar/code.ML	Sat Apr 26 08:34:03 2025 +0200
@@ -1390,10 +1390,7 @@
     fun matches_args args' =
       let
         val k = length args' - length args
-      in if k >= 0
-        then Pattern.matchess thy (args, (map incr_idx o drop k) args')
-        else false
-      end;
+      in k >= 0 andalso Pattern.matchess thy (args, (map incr_idx o drop k) args') end;
     fun drop (thm', proper') = if (proper orelse not proper')
       andalso matches_args (args_of thm') then
         (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^