standardized ML aliases;

--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Apr 11 15:02:48 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Apr 11 20:42:28 2012 +0200
@@ -367,7 +367,7 @@
   case x of
       Term_Func (symbol, tptp_term_list) =>
         "(" ^ string_of_symbol symbol ^ " " ^
-        String.concatWith " " (map string_of_tptp_term tptp_term_list) ^ ")"
+        space_implode " " (map string_of_tptp_term tptp_term_list) ^ ")"
     | Term_Var str => str
     | Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*)
     | Term_Num (_, str) => str
@@ -449,15 +449,15 @@
 
 and string_of_tptp_formula (Pred (symbol, tptp_term_list)) =
       "(" ^ string_of_symbol symbol ^
-      String.concatWith " " (map string_of_tptp_term tptp_term_list) ^ ")"
+      space_implode " " (map string_of_tptp_term tptp_term_list) ^ ")"
   | string_of_tptp_formula (Fmla (symbol, tptp_formula_list)) =
       "(" ^
       string_of_symbol symbol ^
-      String.concatWith " " (map string_of_tptp_formula tptp_formula_list) ^ ")"
+      space_implode " " (map string_of_tptp_formula tptp_formula_list) ^ ")"
   | string_of_tptp_formula (Sequent (tptp_formula_list1, tptp_formula_list2)) = "" (*FIXME*)
   | string_of_tptp_formula (Quant (quantifier, varlist, tptp_formula)) =
       string_of_quantifier quantifier ^ "[" ^
-      String.concatWith ", " (map (fn (n, ty) =>
+      space_implode ", " (map (fn (n, ty) =>
         case ty of
           NONE => n
         | SOME ty => n ^ " : " ^ string_of_tptp_type ty) varlist) ^ "] : (" ^

--- a/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Wed Apr 11 15:02:48 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML	Wed Apr 11 20:42:28 2012 +0200
@@ -83,7 +83,7 @@
    | SOME (rule, ids) =>
        map (dot_arc reverse_arrows
              (n, if with_label then SOME rule else NONE)) ids
-       |> String.concat)
+       |> implode)
  else ""
 
 (*FIXME add opts to label arcs etc*)
@@ -100,7 +100,7 @@
   in
     TPTP_Parser.parse_file input_file
     |> map (tptp_dot_node false true)
-    |> String.concat
+    |> implode
     |> (fn str => "digraph ProofGraph {\n" ^ defaults ^ str ^ "}")
     |> File.write (Path.explode output_file)
   end