# HG changeset patch
# User wenzelm
# Date 1184881742 -7200
# Node ID 4642a2eefe74051f329a2ed343e5099dde59e4e0
# Parent  6c644d14d91d9a1baf504259e7795e869de90feb
added rep_ident;

diff -r 6c644d14d91d -r 4642a2eefe74 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