# HG changeset patch
# User kuncar
# Date 1392298325 -3600
# Node ID a422f93eae0d061e52663b03a6c52cf41de05d0d
# Parent  2cf404a469becbc2a0f38c2a32805b489cfb3b1c
all_args_conv works also for zero arguments

diff -r 2cf404a469be -r a422f93eae0d src/HOL/Tools/Lifting/lifting_util.ML
--- 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