src/HOL/Import/hol4rews.ML

         fun new_name internal isa =
             if internal
             then
                 let
                     val paths = Long_Name.explode isa
-                    val i = Library.drop(length paths - 2,paths)
+                    val i = drop (length paths - 2) paths
                 in
                     case i of
                         [seg,con] => output_thy ^ "." ^ seg ^ "." ^ con
                       | _ => error "hol4rews.dump internal error"
                 end