tuning
authorblanchet
Tue Sep 06 09:11:08 2011 +0200 (2011-09-06)
changeset 44739fd181066602d
parent 44738 1b333e4173a2
child 44741 600d26952759
tuning
src/HOL/Tools/ATP/atp_problem.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Sep 06 09:11:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Sep 06 09:11:08 2011 +0200
     1.3 @@ -263,7 +263,7 @@
     1.4        | str _ (ATyAbs (ss, ty)) =
     1.5          tptp_pi_binder ^ "[" ^
     1.6          commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))
     1.7 -                    ss) ^ "] : " ^ str false ty
     1.8 +                    ss) ^ "]: " ^ str false ty
     1.9    in str true ty end
    1.10  
    1.11  fun string_for_type (THF0 _) ty = str_for_type ty
    1.12 @@ -308,7 +308,7 @@
    1.13         | (_, true, [AAbs ((s', ty), tm)]) =>
    1.14           (*There is code in ATP_Translate to ensure that Eps is always applied
    1.15             to an abstraction*)
    1.16 -         tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "] : " ^
    1.17 +         tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
    1.18             string_for_term format tm ^ ""
    1.19           |> enclose "(" ")"
    1.20  
    1.21 @@ -320,12 +320,12 @@
    1.22               s ^ "(" ^ commas ss ^ ")"
    1.23           end)
    1.24    | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
    1.25 -    "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^
    1.26 +    "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
    1.27      string_for_term format tm ^ ")"
    1.28    | string_for_term _ _ = raise Fail "unexpected term in first-order format"
    1.29  and string_for_formula format (AQuant (q, xs, phi)) =
    1.30      string_for_quantifier q ^
    1.31 -    "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
    1.32 +    "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^
    1.33      string_for_formula format phi
    1.34      |> enclose "(" ")"
    1.35    | string_for_formula format