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) ^ "] : (" ^
2.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML Wed Apr 11 15:02:48 2012 +0200
2.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML Wed Apr 11 20:42:28 2012 +0200
2.3 @@ -83,7 +83,7 @@
2.4 | SOME (rule, ids) =>
2.5 map (dot_arc reverse_arrows
2.6 (n, if with_label then SOME rule else NONE)) ids
2.7 - |> String.concat)
2.8 + |> implode)
2.9 else ""
2.10
2.11 (*FIXME add opts to label arcs etc*)
2.12 @@ -100,7 +100,7 @@
2.13 in
2.14 TPTP_Parser.parse_file input_file
2.15 |> map (tptp_dot_node false true)
2.16 - |> String.concat
2.17 + |> implode
2.18 |> (fn str => "digraph ProofGraph {\n" ^ defaults ^ str ^ "}")
2.19 |> File.write (Path.explode output_file)
2.20 end