src/Pure/General/path.ML

           SOME s' => variable_elem s'
         | NONE => basic_elem s))
       handle ERROR msg => cat_error msg ("The error(s) above occurred in " ^ quote str);
 
     val (roots, raw_elems) =
-      (case take_prefix (equal "") (space_explode "/" str) |>> length of
+      (case chop_prefix (equal "") (space_explode "/" str) |>> length of
         (0, es) => ([], es)
       | (1, es) => ([Root ""], es)
       | (_, []) => ([Root ""], [])
       | (_, e :: es) => ([root_elem e], es));
     val elems = raw_elems |> filter_out (fn c => c = "" orelse c = ".") |> map explode_elem;

 
 fun ext "" = I
   | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
 
 val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
-  (case take_suffix (fn c => c <> ".") (raw_explode s) of
+  (case chop_suffix (fn c => c <> ".") (raw_explode s) of
     ([], _) => (Path [Basic s], "")
   | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
 
 
 (* expand variables *)