# HG changeset patch
# User wenzelm
# Date 1244135757 -7200
# Node ID d24ef3ff34bc3c78461ea43b4a82b22c10a6f499
# Parent  1f9b6a5dc8cc993119c79f3203a82ea59f851b15
export file_name;

diff -r 1f9b6a5dc8cc -r d24ef3ff34bc src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Thu Jun 04 19:15:55 2009 +0200
+++ b/src/Pure/General/position.ML	Thu Jun 04 19:15:57 2009 +0200
@@ -16,6 +16,7 @@
   val distance_of: T -> T -> int
   val none: T
   val start: T
+  val file_name: string -> Properties.T
   val file: string -> T
   val line: int -> T
   val line_file: int -> string -> T