src/Pure/General/url.ML
changeset 19305 5c16895d548b
parent 16195 0eb3c15298cd
child 21503 c4ea7e8c3937
     1.1 --- a/src/Pure/General/url.ML	Tue Mar 21 12:18:13 2006 +0100
     1.2 +++ b/src/Pure/General/url.ML	Tue Mar 21 12:18:15 2006 +0100
     1.3 @@ -53,7 +53,7 @@
     1.4  local
     1.5  
     1.6  val scan_host =
     1.7 -  (Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode) --|
     1.8 +  (Scan.any1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
     1.9    Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
    1.10  
    1.11  val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);