# HG changeset patch
# User blanchet
# Date 1369042555 -7200
# Node ID bc053db0801e8325274a6fd672ce956dcbc064a6
# Parent  ccb292952774cf4c8f5237056658d7051a5b0a78
tuned code

diff -r ccb292952774 -r bc053db0801e src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon May 20 11:27:13 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon May 20 11:35:55 2013 +0200
@@ -418,33 +418,42 @@
 
 fun tptp_string_of_term _ (ATerm ((s, []), [])) = s
   | tptp_string_of_term format (ATerm ((s, tys), ts)) =
-    (if s = tptp_empty_list then
-       (* used for lists in the optional "source" field of a derivation *)
-       "[" ^ commas (map (tptp_string_of_term format) ts) ^ "]"
-     else if is_tptp_equal s then
-       space_implode (" " ^ tptp_equal ^ " ")
-                     (map (tptp_string_of_term format) ts)
-       |> is_format_higher_order format ? enclose "(" ")"
-     else case (s = tptp_ho_forall orelse s = tptp_ho_exists, s = tptp_choice,
-                ts) of
-       (true, _, [AAbs (((s', ty), tm), [])]) =>
-       (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
-          possible, to work around LEO-II 1.2.8 parser limitation. *)
-       tptp_string_of_formula format
-           (AQuant (if s = tptp_ho_forall then AForall else AExists,
-                    [(s', SOME ty)], AAtom tm))
-     | (_, true, [AAbs (((s', ty), tm), args)]) =>
-       (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always
-          applied to an abstraction. *)
-       tptp_string_of_app format
-           (tptp_choice ^ "[" ^ s' ^ " : " ^ string_of_type format ty ^ "]: " ^
-            tptp_string_of_term format tm ^ ""
-            |> enclose "(" ")")
-           (map (tptp_string_of_term format) args)
-     | _ =>
-       tptp_string_of_app format s
-           (map (string_of_type format) tys
-            @ map (tptp_string_of_term format) ts))
+    let
+      fun app () =
+        tptp_string_of_app format s
+            (map (string_of_type format) tys @
+             map (tptp_string_of_term format) ts)
+    in
+      if s = tptp_empty_list then
+        (* used for lists in the optional "source" field of a derivation *)
+        "[" ^ commas (map (tptp_string_of_term format) ts) ^ "]"
+      else if is_tptp_equal s then
+        space_implode (" " ^ tptp_equal ^ " ")
+                      (map (tptp_string_of_term format) ts)
+        |> is_format_higher_order format ? enclose "(" ")"
+      else if s = tptp_ho_forall orelse s = tptp_ho_exists then
+        case ts of
+          [AAbs (((s', ty), tm), [])] =>
+          (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
+             possible, to work around LEO-II 1.2.8 parser limitation. *)
+          tptp_string_of_formula format
+              (AQuant (if s = tptp_ho_forall then AForall else AExists,
+                      [(s', SOME ty)], AAtom tm))
+        | _ => app ()
+      else if s = tptp_choice then
+        case ts of
+          [AAbs (((s', ty), tm), args)] =>
+          (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is
+             always applied to an abstraction. *)
+          tptp_string_of_app format
+              (tptp_choice ^ "[" ^ s' ^ " : " ^ string_of_type format ty ^
+               "]: " ^ tptp_string_of_term format tm ^ ""
+               |> enclose "(" ")")
+              (map (tptp_string_of_term format) args)
+        | _ => app ()
+      else
+        app ()
+    end
   | tptp_string_of_term (format as THF _) (AAbs (((s, ty), tm), args)) =
     tptp_string_of_app format
         ("(^[" ^ s ^ " : " ^ string_of_type format ty ^ "]: " ^