src/HOL/Tools/Datatype/datatype.ML

     val named_rules = flat (map_index (fn (index, tname) =>
       [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
        ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
     val unnamed_rules = map (fn induct =>
       ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""]))
-        (Library.drop (length dt_names, inducts));
+        ((uncurry drop) (length dt_names, inducts));
   in
     thy9
     |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
         ((prfx (Binding.name "inducts"), inducts), []),
         ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []),