# HG changeset patch
# User blanchet
# Date 1446497389 -3600
# Node ID 16e2313e855cf6786941d9a0d19ea25dbd15ff6f
# Parent  5e955ac3fddab8988470333e624c4687e83e0c6a
make sure that function types are never generated as '> @ A @ B', but always as 'A > B'

diff -r 5e955ac3fdda -r 16e2313e855c src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Nov 02 20:11:16 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Nov 02 21:49:49 2015 +0100
@@ -397,15 +397,20 @@
     val dfg = (case format of DFG _ => true | _ => false)
     fun str _ (AType ((s, _), [])) =
         if dfg andalso s = tptp_individual_type then dfg_individual_type else s
-      | str _ (AType ((s, _), tys)) =
-        let val ss = tys |> map (str false) in
-          if s = tptp_product_type then
-            ss |> space_implode
-                      (if dfg then ", " else " " ^ tptp_product_type ^ " ")
-               |> (not dfg andalso length ss > 1) ? parens
-          else
-            tptp_string_of_app format s ss
-        end
+      | str rhs (AType ((s, _), tys)) =
+        if s = tptp_fun_type then
+          let val [ty1, ty2] = tys in
+            str rhs (AFun (ty1, ty2))
+          end
+        else
+          let val ss = tys |> map (str false) in
+            if s = tptp_product_type then
+              ss |> space_implode
+                        (if dfg then ", " else " " ^ tptp_product_type ^ " ")
+                 |> (not dfg andalso length ss > 1) ? parens
+            else
+              tptp_string_of_app format s ss
+          end
       | str rhs (AFun (ty1, ty2)) =
         (str false ty1 |> dfg ? parens) ^ " " ^
         (if dfg then "" else tptp_fun_type ^ " ") ^ str true ty2