diff -r 488046fdda59 -r cf43583f9bb9 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Jun 16 16:18:15 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Jun 16 16:18:34 2014 +0200
@@ -94,7 +94,6 @@
   val tptp_true : string
   val tptp_lambda : string
   val tptp_empty_list : string
-  val tptp_binary_op_list : string list
   val isabelle_info_prefix : string
   val isabelle_info : string -> int -> (string, 'a) atp_term list
   val extract_isabelle_status : (string, 'a) atp_term list -> string option
@@ -249,8 +248,6 @@
 val tptp_true = "$true"
 val tptp_lambda = "^"
 val tptp_empty_list = "[]"
-val tptp_binary_op_list = [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if,
-                             tptp_iff, tptp_not_iff, tptp_equal, tptp_app]
 val isabelle_info_prefix = "isabelle_"
 
 val inductionN = "induction"