--- a/src/Pure/General/file.ML Wed May 18 11:30:58 2005 +0200 +++ b/src/Pure/General/file.ML Wed May 18 11:30:59 2005 +0200 @@ -96,7 +96,7 @@ | s => SOME (Info s)) end; -val exists = isSome o info; +val exists = is_some o info; (* directories *)