src/Pure/Isar/code.ML

     val args_of = snd o strip_comb o map_types Type.strip_sorts
       o fst o Logic.dest_equals o Thm.plain_prop_of;
     val args = args_of thm;
     val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
     fun matches_args args' = length args <= length args' andalso
-      Pattern.matchess thy (args, (map incr_idx o curry (uncurry take) (length args)) args');
+      Pattern.matchess thy (args, (map incr_idx o take (length args)) args');
     fun drop (thm', proper') = if (proper orelse not proper')
       andalso matches_args (args_of thm') then 
         (warning ("Code generator: dropping redundant code equation\n" ^
             Display.string_of_thm_global thy thm'); true)
       else false;