standardized ML aliases;
authorwenzelm
Wed, 11 Apr 2012 20:42:28 +0200
changeset 4829726c1a97c7784
parent 48296 45e570742e73
child 48298 0daa97ed1585
standardized ML aliases;
src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML
     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