# HG changeset patch
# User wenzelm
# Date 1184015556 -7200
# Node ID 3fd7770f679543437d20aa9e67e1004c1fac7e2c
# Parent  9e8257472c27d99046ebb32680d0ad7a88d116d0
moved Path.position to Position.path;

diff -r 9e8257472c27 -r 3fd7770f6795 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Mon Jul 09 23:12:35 2007 +0200
+++ b/src/Pure/General/path.ML	Mon Jul 09 23:12:36 2007 +0200
@@ -28,7 +28,6 @@
   val ext: string -> T -> T
   val split_ext: T -> T * string
   val expand: T -> T
-  val position: T -> Position.T
 end;
 
 structure Path: PATH =
@@ -154,7 +153,6 @@
   | eval x = [x];
 
 val expand = rep #> maps eval #> norm #> Path;
-val position = expand #> implode_path #> quote #> Position.line_name 1;
 
 
 (*final declarations of this structure!*)