# HG changeset patch
# User blanchet
# Date 1314967400 -7200
# Node ID dbdfadbd38299be1c397340043b75859c040fdde
# Parent  3d7b737d200af70cd14552dd50a0c455e312a6ef
use new syntax for Pi binder in TFF1 output

diff -r 3d7b737d200a -r dbdfadbd3829 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Fri Sep 02 14:43:20 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Sep 02 14:43:20 2011 +0200
@@ -53,6 +53,7 @@
   val tptp_product_type : string
   val tptp_forall : string
   val tptp_ho_forall : string
+  val tptp_pi_binder : string
   val tptp_exists : string
   val tptp_ho_exists : string
   val tptp_choice : string
@@ -160,6 +161,7 @@
 val tptp_product_type = "*"
 val tptp_forall = "!"
 val tptp_ho_forall = "!!"
+val tptp_pi_binder = "!>"
 val tptp_exists = "?"
 val tptp_ho_exists = "??"
 val tptp_choice = "@+"
@@ -259,7 +261,7 @@
         str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
         |> not rhs ? enclose "(" ")"
       | str _ (ATyAbs (ss, ty)) =
-        tptp_forall ^ "[" ^
+        tptp_pi_binder ^ "[" ^
         commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))
                     ss) ^ "] : " ^ str false ty
   in str true ty end