src/Pure/General/file.ML

--- 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