moved Path.position to Position.path;
authorwenzelm
Mon, 09 Jul 2007 23:12:36 +0200
changeset 23672 3fd7770f6795
parent 23671 9e8257472c27
child 23673 67c748e5ae54
moved Path.position to Position.path;
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!*)