moved Path.position to Position.path;
authorwenzelm
Mon Jul 09 23:12:36 2007 +0200 (2007-07-09)
changeset 236723fd7770f6795
parent 23671 9e8257472c27
child 23673 67c748e5ae54
moved Path.position to Position.path;
src/Pure/General/path.ML
     1.1 --- a/src/Pure/General/path.ML	Mon Jul 09 23:12:35 2007 +0200
     1.2 +++ b/src/Pure/General/path.ML	Mon Jul 09 23:12:36 2007 +0200
     1.3 @@ -28,7 +28,6 @@
     1.4    val ext: string -> T -> T
     1.5    val split_ext: T -> T * string
     1.6    val expand: T -> T
     1.7 -  val position: T -> Position.T
     1.8  end;
     1.9  
    1.10  structure Path: PATH =
    1.11 @@ -154,7 +153,6 @@
    1.12    | eval x = [x];
    1.13  
    1.14  val expand = rep #> maps eval #> norm #> Path;
    1.15 -val position = expand #> implode_path #> quote #> Position.line_name 1;
    1.16  
    1.17  
    1.18  (*final declarations of this structure!*)