src/Pure/General/path.ML
changeset 15531 08c8dad8e399
parent 14981 e73f8140af78
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/General/path.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/General/path.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4  
     1.5  fun split_path f (path as Path xs) =
     1.6    (case try split_last xs of
     1.7 -    Some (prfx, Basic s) => f (prfx, s)
     1.8 +    SOME (prfx, Basic s) => f (prfx, s)
     1.9    | _ => error ("Cannot split path into dir/base: " ^ quote (pack path)));
    1.10  
    1.11  val dir = split_path (fn (prfx, _) => Path prfx);