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.
all_args_conv works also for zero arguments
authorkuncar
Thu, 13 Feb 2014 14:32:05 +0100
changeset 55456 a422f93eae0d
parent 55455 2cf404a469be
child 55457 e373c9f60db1
all_args_conv works also for zero arguments
src/HOL/Tools/Lifting/lifting_util.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Thu Feb 13 14:32:04 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Thu Feb 13 14:32:05 2014 +0100
@@ -95,8 +95,7 @@
 
 fun strip_args n = funpow n (fst o dest_comb)
 
-fun all_args_conv conv ctm = 
-  (Conv.combination_conv (Conv.try_conv (all_args_conv conv)) conv) ctm
+fun all_args_conv conv ctm = Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm
 
 fun is_Type (Type _) = true
   | is_Type _ = false
isabelle