# HG changeset patch
# User blanchet
# Date 1315293068 -7200
# Node ID fd181066602da1f4291bcd78a6f21b2c25bb9d9c
# Parent  1b333e4173a20452b9a3cae57427cc8ebd2ff953
tuning

diff -r 1b333e4173a2 -r fd181066602d src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Sep 06 09:11:08 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Sep 06 09:11:08 2011 +0200
@@ -263,7 +263,7 @@
       | str _ (ATyAbs (ss, ty)) =
         tptp_pi_binder ^ "[" ^
         commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))
-                    ss) ^ "] : " ^ str false ty
+                    ss) ^ "]: " ^ str false ty
   in str true ty end
 
 fun string_for_type (THF0 _) ty = str_for_type ty
@@ -308,7 +308,7 @@
        | (_, true, [AAbs ((s', ty), tm)]) =>
          (*There is code in ATP_Translate to ensure that Eps is always applied
            to an abstraction*)
-         tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "] : " ^
+         tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
            string_for_term format tm ^ ""
          |> enclose "(" ")"
 
@@ -320,12 +320,12 @@
              s ^ "(" ^ commas ss ^ ")"
          end)
   | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
-    "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^
+    "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
     string_for_term format tm ^ ")"
   | string_for_term _ _ = raise Fail "unexpected term in first-order format"
 and string_for_formula format (AQuant (q, xs, phi)) =
     string_for_quantifier q ^
-    "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
+    "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^
     string_for_formula format phi
     |> enclose "(" ")"
   | string_for_formula format