# HG changeset patch
# User blanchet
# Date 1306224060 -7200
# Node ID 13cb8895f53815b2a8a8a4830162561de8d44e27
# Parent  4e2d6c1e5392f9ab6e00dba2a652e0cddd057897
tuning

diff -r 4e2d6c1e5392 -r 13cb8895f538 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue May 24 10:00:38 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue May 24 10:01:00 2011 +0200
@@ -27,13 +27,15 @@
 
   (* official TPTP syntax *)
   val tptp_special_prefix : string
+  val tptp_has_type : string
   val tptp_type_of_types : string
   val tptp_bool_type : string
   val tptp_individual_type : string
   val tptp_fun_type : string
   val tptp_false : string
   val tptp_true : string
-  val tptp_app_op : string
+  val tptp_not : string
+  val tptp_app : string
   val is_atp_variable : string -> bool
   val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
   val mk_aconn :
@@ -77,13 +79,15 @@
 
 (* official TPTP syntax *)
 val tptp_special_prefix = "$"
+val tptp_has_type = ":"
 val tptp_type_of_types = "$tType"
 val tptp_bool_type = "$o"
 val tptp_individual_type = "$i"
 val tptp_fun_type = ">"
 val tptp_false = "$false"
 val tptp_true = "$true"
-val tptp_app_op = "@"
+val tptp_not = "~"
+val tptp_app = "@"
 
 fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
 
@@ -145,7 +149,7 @@
 fun string_for_quantifier AForall = "!"
   | string_for_quantifier AExists = "?"
 
-fun string_for_connective ANot = "~"
+fun string_for_connective ANot = tptp_not
   | string_for_connective AAnd = "&"
   | string_for_connective AOr = "|"
   | string_for_connective AImplies = "=>"
@@ -206,8 +210,6 @@
 
 (** CNF UEQ (Waldmeister) **)
 
-exception LOST_CONJECTURE of unit
-
 fun is_problem_line_negated (Formula (_, _, AConn (ANot, _), _, _)) = true
   | is_problem_line_negated _ = false