src/Pure/General/path.ML
changeset 33955 fff6f11b1f09
parent 33049 c38f02fdf35d
child 33957 e9afca2118d4
     1.1 --- a/src/Pure/General/path.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/Pure/General/path.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -139,7 +139,7 @@
     1.4  val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
     1.5    (case take_suffix (fn c => c <> ".") (explode s) of
     1.6      ([], _) => (Path [Basic s], "")
     1.7 -  | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));
     1.8 +  | (cs, e) => (Path [Basic (implode ((uncurry take) (length cs - 1, cs)))], implode e)));
     1.9  
    1.10  
    1.11  (* expand variables *)