src/HOL/Tools/inductive.ML

--- a/src/HOL/Tools/inductive.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -217,7 +217,7 @@
 fun make_bool_args' xs =
   make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs;
 
-fun arg_types_of k c = Library.drop (k, binder_types (fastype_of c));
+fun arg_types_of k c = (uncurry drop) (k, binder_types (fastype_of c));
 
 fun find_arg T x [] = sys_error "find_arg"
   | find_arg T x ((p as (_, (SOME _, _))) :: ps) =