--- a/src/Pure/General/file.ML Thu Jul 19 23:49:00 2007 +0200
+++ b/src/Pure/General/file.ML Thu Jul 19 23:49:02 2007 +0200
@@ -20,6 +20,7 @@
val isatool: string -> int
val system_command: string -> unit
eqtype ident
+ val rep_ident: ident -> string
val ident: Path.T -> ident option
val exists: Path.T -> bool
val check: Path.T -> unit
@@ -88,6 +89,8 @@
datatype ident = Ident of string;
+fun rep_ident (Ident s) = s;
+
fun ident path =
(case try OS.FileSys.modTime (platform_path path) of
NONE => NONE