diff -r 0c188a3c671a -r 994ebb795b75 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Oct 24 10:03:20 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Oct 24 12:43:33 2013 +0200
@@ -33,14 +33,13 @@
 
   datatype polymorphism = Monomorphic | Polymorphic
   datatype thf_choice = THF_Without_Choice | THF_With_Choice
-  datatype thf_defs = THF_Without_Defs | THF_With_Defs
 
   datatype atp_format =
     CNF |
     CNF_UEQ |
     FOF |
     TFF of polymorphism |
-    THF of polymorphism * thf_choice * thf_defs |
+    THF of polymorphism * thf_choice |
     DFG of polymorphism
 
   datatype atp_formula_role =
@@ -179,14 +178,13 @@
 
 datatype polymorphism = Monomorphic | Polymorphic
 datatype thf_choice = THF_Without_Choice | THF_With_Choice
-datatype thf_defs = THF_Without_Defs | THF_With_Defs
 
 datatype atp_format =
   CNF |
   CNF_UEQ |
   FOF |
   TFF of polymorphism |
-  THF of polymorphism * thf_choice * thf_defs |
+  THF of polymorphism * thf_choice |
   DFG of polymorphism
 
 datatype atp_formula_role =