src/Pure/General/path.ML
changeset 19482 9f11af8f7ef9
parent 19305 5c16895d548b
child 21858 05f57309170c
     1.1 --- a/src/Pure/General/path.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/General/path.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4      | path => rep (unpack path))
     1.5    | eval x = [x];
     1.6  
     1.7 -val expand = rep #> map eval #> List.concat #> norm #> Path;
     1.8 +val expand = rep #> maps eval #> norm #> Path;
     1.9  val position = expand #> pack #> quote #> Position.line_name 1;
    1.10  
    1.11  end;