diff -r 15f001295a7b -r 5c16895d548b src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/General/url.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -53,7 +53,7 @@
 local
 
 val scan_host =
-  (Scan.any1 (not_equal "/" andf Symbol.not_eof) >> implode) --|
+  (Scan.any1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
 
 val scan_path = Scan.any Symbol.not_eof >> (Path.unpack o implode);