# HG changeset patch
# User wenzelm
# Date 1310131060 -7200
# Node ID c37a1f29bbc07aff7adbf9dfa88599fa1d925e1f
# Parent  24fb44c1086a35118a672299cca605f36d1b742b
standardized String.concat towards implode;

diff -r 24fb44c1086a -r c37a1f29bbc0 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Jul 08 14:37:19 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Jul 08 15:17:40 2011 +0200
@@ -886,7 +886,7 @@
            (proved, []) =>
              (Thm.join_proofs (maps (the o #2 o snd) proved);
               File.write (Path.ext "prv" path)
-                (concat (map (fn (s, _) => snd (strip_number s) ^
+                (implode (map (fn (s, _) => snd (strip_number s) ^
                    " -- proved by " ^ Distribution.version ^ "\n") proved));
               {pfuns = pfuns, type_map = type_map, env = NONE})
          | (_, unproved) => err_vcs (map fst unproved))
diff -r 24fb44c1086a -r c37a1f29bbc0 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Fri Jul 08 14:37:19 2011 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Fri Jul 08 15:17:40 2011 +0200
@@ -30,6 +30,7 @@
 val _ = PolyML.Compiler.forgetValue "foldr";
 val _ = PolyML.Compiler.forgetValue "print";
 val _ = PolyML.Compiler.forgetValue "explode";
+val _ = PolyML.Compiler.forgetValue "concat";
 
 
 (* Compiler options *)
diff -r 24fb44c1086a -r c37a1f29bbc0 src/Tools/WWW_Find/http_util.ML
--- a/src/Tools/WWW_Find/http_util.ML	Fri Jul 08 14:37:19 2011 +0200
+++ b/src/Tools/WWW_Find/http_util.ML	Fri Jul 08 15:17:40 2011 +0200
@@ -17,7 +17,7 @@
 
 val crlf = "\r\n";
 
-fun make_header_field (name, value) = concat [name, ": ", value, crlf];
+fun make_header_field (name, value) = implode [name, ": ", value, crlf];
 
 fun reply_header (status, content_type, extra_fields) =
   let
@@ -25,9 +25,9 @@
     val reason = HttpStatus.to_reason status;
     val show_content_type = pair "Content-Type" o Mime.show_type;
   in
-  concat
+  implode
     (map make_header_field
-      (("Status", concat [code, " ", reason])
+      (("Status", implode [code, " ", reason])
        :: (the_list o Option.map show_content_type) content_type
        @ extra_fields)
     @ [crlf])
@@ -89,7 +89,7 @@
 val make_query_string =
   Symtab.dest
   #> map join_pairs
-  #> String.concatWith "&";
+  #> space_implode "&";
 
 end;
 
diff -r 24fb44c1086a -r c37a1f29bbc0 src/Tools/WWW_Find/mime.ML
--- a/src/Tools/WWW_Find/mime.ML	Fri Jul 08 14:37:19 2011 +0200
+++ b/src/Tools/WWW_Find/mime.ML	Fri Jul 08 15:17:40 2011 +0200
@@ -37,10 +37,10 @@
   #> apsnd (Substring.triml 1)
   #> pairself (Substring.string o strip);
 
-fun show_param (n, v) = concat ["; ", n, "=", v];
+fun show_param (n, v) = implode ["; ", n, "=", v];
 
 fun show_type (Type {main, sub, params}) =
-      concat ([main, "/", sub] @ map show_param params);
+  implode ([main, "/", sub] @ map show_param params);
 
 fun parse_type s =
   (case Substring.fields (Char.contains "/;") (Substring.full s) of
diff -r 24fb44c1086a -r c37a1f29bbc0 src/Tools/WWW_Find/scgi_req.ML
--- a/src/Tools/WWW_Find/scgi_req.ML	Fri Jul 08 14:37:19 2011 +0200
+++ b/src/Tools/WWW_Find/scgi_req.ML	Fri Jul 08 15:17:40 2011 +0200
@@ -129,7 +129,7 @@
         fun show (n, v) r = ["\t", n, " = \"", to_string v, "\"\n"] @ r;
       in Symtab.fold show table [] end;
   in
-    concat
+    implode
       (["path_info: \"", path_info, "\"\n",
         "path_translated: \"", path_translated, "\"\n",
         "script_name: \"", script_name, "\"\n",
diff -r 24fb44c1086a -r c37a1f29bbc0 src/Tools/WWW_Find/socket_util.ML
--- a/src/Tools/WWW_Find/socket_util.ML	Fri Jul 08 14:37:19 2011 +0200
+++ b/src/Tools/WWW_Find/socket_util.ML	Fri Jul 08 15:17:40 2011 +0200
@@ -41,7 +41,7 @@
     val (haddr, port) = INetSock.fromAddr (Socket.Ctl.getSockName sock);
 
     val sock_name =
-      String.concat [ NetHostDB.toString haddr, ":", string_of_int port ];
+      implode [ NetHostDB.toString haddr, ":", string_of_int port ];
 
     val rd =
       BinPrimIO.RD {
diff -r 24fb44c1086a -r c37a1f29bbc0 src/Tools/WWW_Find/xhtml.ML
--- a/src/Tools/WWW_Find/xhtml.ML	Fri Jul 08 14:37:19 2011 +0200
+++ b/src/Tools/WWW_Find/xhtml.ML	Fri Jul 08 15:17:40 2011 +0200
@@ -169,7 +169,7 @@
 fun append (Tag (nm, atts, inner)) inner' = Tag (nm, atts, inner @ inner')
   | append _ _ = raise Fail "cannot append to a text element";
 
-fun show_att (n, v) = concat [" ", n, "=\"", XML.text v, "\""];
+fun show_att (n, v) = implode [" ", n, "=\"", XML.text v, "\""];
 
 fun show_text (Text t) = XML.text t
   | show_text (RawText t) = t