# HG changeset patch
# User blanchet
# Date 1382611413 -7200
# Node ID 994ebb795b752707c46eb7ca9a40491efb2cea1f
# Parent  0c188a3c671a598d25e1b85373a8e1aed2d04ebc
use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations

diff -r 0c188a3c671a -r 994ebb795b75 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Thu Oct 24 10:03:20 2013 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Thu Oct 24 12:43:33 2013 +0200
@@ -34,8 +34,8 @@
 val prefix = Library.prefix
 val fact_name_of = prefix fact_prefix o ascii_of
 
-fun atp_of_format (THF (Polymorphic, _, _)) = dummy_thfN
-  | atp_of_format (THF (Monomorphic, _, _)) = satallaxN
+fun atp_of_format (THF (Polymorphic, _)) = dummy_thfN
+  | atp_of_format (THF (Monomorphic, _)) = satallaxN
   | atp_of_format (DFG Polymorphic) = spass_polyN
   | atp_of_format (DFG Monomorphic) = spassN
   | atp_of_format (TFF Polymorphic) = alt_ergoN
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 =
diff -r 0c188a3c671a -r 994ebb795b75 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Oct 24 10:03:20 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Oct 24 12:43:33 2013 +0200
@@ -697,11 +697,9 @@
     Raw_Polymorphic With_Phantom_Type_Vars
   | no_type_classes poly = poly
 
-fun adjust_type_enc (THF (Polymorphic, choice, _))
-                    (Native (order, poly, level)) =
+fun adjust_type_enc (THF (Polymorphic, choice)) (Native (order, poly, level)) =
     Native (adjust_order choice order, no_type_classes poly, level)
-  | adjust_type_enc (THF (Monomorphic, choice, _))
-                         (Native (order, _, level)) =
+  | adjust_type_enc (THF (Monomorphic, choice)) (Native (order, _, level)) =
     Native (adjust_order choice order, Mangled_Monomorphic, level)
   | adjust_type_enc (TFF Monomorphic) (Native (_, _, level)) =
     Native (First_Order, Mangled_Monomorphic, level)
@@ -1317,7 +1315,7 @@
      atomic_types = atomic_Ts}
   end
 
-fun is_format_with_defs (THF (_, _, THF_With_Defs)) = true
+fun is_format_with_defs (THF _) = true
   | is_format_with_defs _ = false
 
 fun make_fact ctxt format type_enc iff_for_eq
diff -r 0c188a3c671a -r 994ebb795b75 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Oct 24 10:03:20 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Oct 24 12:43:33 2013 +0200
@@ -211,7 +211,7 @@
 
 (* agsyHOL *)
 
-val agsyhol_thf0 = THF (Monomorphic, THF_Without_Choice, THF_With_Defs)
+val agsyhol_thf0 = THF (Monomorphic, THF_Without_Choice)
 
 val agsyhol_config : atp_config =
   {exec = K (["AGSYHOL_HOME"], ["agsyHOL"]),
@@ -461,7 +461,7 @@
 
 (* LEO-II supports definitions, but it performs significantly better on our
    benchmarks when they are not used. *)
-val leo2_thf0 = THF (Monomorphic, THF_Without_Choice, THF_Without_Defs)
+val leo2_thf0 = THF (Monomorphic, THF_Without_Choice)
 
 val leo2_config : atp_config =
   {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
@@ -488,7 +488,7 @@
 (* Satallax *)
 
 (* Choice is disabled until there is proper reconstruction for it. *)
-val satallax_thf0 = THF (Monomorphic, THF_Without_Choice, THF_With_Defs)
+val satallax_thf0 = THF (Monomorphic, THF_Without_Choice)
 
 val satallax_config : atp_config =
   {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
@@ -653,7 +653,7 @@
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
-val dummy_thf_format = THF (Polymorphic, THF_With_Choice, THF_With_Defs)
+val dummy_thf_format = THF (Polymorphic, THF_With_Choice)
 val dummy_thf_config =
   dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)