Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorhaftmann
Sat, 26 Apr 2025 08:34:03 +0200
changeset 82586 e55d712eff7b
parent 82585 46591222e4fc
child 82592 a151c934824c
tuned
src/Pure/Isar/code.ML file | annotate | diff | comparison | revisions 
--- 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" ^
isabelle