1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Apr 11 15:02:48 2012 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Apr 11 20:42:28 2012 +0200
     1.3 @@ -367,7 +367,7 @@
     1.4    case x of
     1.5        Term_Func (symbol, tptp_term_list) =>
     1.6          "(" ^ string_of_symbol symbol ^ " " ^
     1.7 -        String.concatWith " " (map string_of_tptp_term tptp_term_list) ^ ")"
     1.8 +        space_implode " " (map string_of_tptp_term tptp_term_list) ^ ")"
     1.9      | Term_Var str => str
    1.10      | Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*)
    1.11      | Term_Num (_, str) => str
    1.12 @@ -449,15 +449,15 @@
    1.13  
    1.14  and string_of_tptp_formula (Pred (symbol, tptp_term_list)) =
    1.15        "(" ^ string_of_symbol symbol ^
    1.16 -      String.concatWith " " (map string_of_tptp_term tptp_term_list) ^ ")"
    1.17 +      space_implode " " (map string_of_tptp_term tptp_term_list) ^ ")"
    1.18    | string_of_tptp_formula (Fmla (symbol, tptp_formula_list)) =
    1.19        "(" ^
    1.20        string_of_symbol symbol ^
    1.21 -      String.concatWith " " (map string_of_tptp_formula tptp_formula_list) ^ ")"
    1.22 +      space_implode " " (map string_of_tptp_formula tptp_formula_list) ^ ")"
    1.23    | string_of_tptp_formula (Sequent (tptp_formula_list1, tptp_formula_list2)) = "" (*FIXME*)
    1.24    | string_of_tptp_formula (Quant (quantifier, varlist, tptp_formula)) =
    1.25        string_of_quantifier quantifier ^ "[" ^
    1.26 -      String.concatWith ", " (map (fn (n, ty) =>
    1.27 +      space_implode ", " (map (fn (n, ty) =>
    1.28          case ty of
    1.29            NONE => n
    1.30          | SOME ty => n ^ " : " ^ string_of_tptp_type ty) varlist) ^ "] : (" ^