src/HOL/Tools/inductive.ML
changeset 33955 fff6f11b1f09
parent 33766 c679f05600cd
child 33957 e9afca2118d4
     1.1 --- a/src/HOL/Tools/inductive.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -217,7 +217,7 @@
     1.4  fun make_bool_args' xs =
     1.5    make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs;
     1.6  
     1.7 -fun arg_types_of k c = Library.drop (k, binder_types (fastype_of c));
     1.8 +fun arg_types_of k c = (uncurry drop) (k, binder_types (fastype_of c));
     1.9  
    1.10  fun find_arg T x [] = sys_error "find_arg"
    1.11    | find_arg T x ((p as (_, (SOME _, _))) :: ps) =