added rep_ident;
authorwenzelm
Thu, 19 Jul 2007 23:49:02 +0200
changeset 23874 4642a2eefe74
parent 23873 6c644d14d91d
child 23875 e22705ccc07d
added rep_ident;
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