diff --git a/src/Pure/General/url.ML b/src/Pure/General/url.ML
--- a/src/Pure/General/url.ML
+++ b/src/Pure/General/url.ML
@@ -1,94 +1,59 @@
 (*  Title:      Pure/General/url.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
-Basic URLs, see RFC 1738 and RFC 2396.
+Basic URLs (see RFC 1738 and RFC 2396).
 *)
 
 signature URL =
 sig
   datatype T =
     File of Path.T |
     Http of string * Path.T |
     Https of string * Path.T |
     Ftp of string * Path.T
-  val append: T -> T -> T
-  val implode: T -> string
   val explode: string -> T
-  val pretty: T -> Pretty.T
-  val print: T -> string
 end;
 
 structure Url: URL =
 struct
 
 (* type url *)
 
 datatype T =
   File of Path.T |
   Http of string * Path.T |
   Https of string * Path.T |
   Ftp of string * Path.T;
 
 
-(* append *)
-
-fun append (File p) (File p') = File (p + p')
-  | append (Http (h, p)) (File p') = Http (h, p + p')
-  | append (Https (h, p)) (File p') = Https (h, p + p')
-  | append (Ftp (h, p)) (File p') = Ftp (h, p + p')
-  | append _ url = url;
-
-
-(* implode *)
-
-fun implode_path p = if Path.is_current p then "" else Path.implode p;
-
-fun implode_url (File p) = implode_path p
-  | implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
-  | implode_url (Https (h, p)) = "https://" ^ h ^ implode_path p
-  | implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
-
-
 (* explode *)
 
 local
 
 val scan_host =
   (Scan.many1 (fn s => s <> "/" andalso Symbol.not_eof s) >> implode) --|
   Scan.ahead ($$ "/" || Scan.one Symbol.is_eof);
 
 val scan_path = Scan.many Symbol.not_eof >> (Path.explode o implode);
 val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
 
 val scan_url =
   Scan.unless
     (Scan.this_string "file:" || Scan.this_string "http:" ||
       Scan.this_string "https:" || Scan.this_string "ftp:") scan_path >> File ||
   Scan.this_string "file:///" |-- scan_path_root >> File ||
   Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
   Scan.this_string "file://" |-- scan_host -- scan_path
     >> (fn (h, p) => File (Path.named_root h + p)) ||
   Scan.this_string "file:/" |-- scan_path_root >> File ||
   Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
   Scan.this_string "https://" |-- scan_host -- scan_path >> Https ||
   Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
 
 in
 
-fun explode_url s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
+fun explode s = Symbol.scanner "Malformed URL" scan_url (Symbol.explode s);
 
 end;
 
-
-(* print *)
-
-val pretty = Pretty.mark_str o `Markup.url o implode_url;
-
-val print = Pretty.unformatted_string_of o pretty;
-
-
-(*final declarations of this structure!*)
-val implode = implode_url;
-val explode = explode_url;
-
 end;