--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Nov 26 18:06:36 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Nov 26 18:45:19 2020 +0100
@@ -33,7 +33,7 @@
datatype fool = Without_FOOL | With_FOOL
datatype polymorphism = Monomorphic | Polymorphic
- datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice
+ datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
datatype atp_format =
CNF |
@@ -193,7 +193,7 @@
datatype fool = Without_FOOL | With_FOOL
datatype polymorphism = Monomorphic | Polymorphic
-datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice
+datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
datatype atp_format =
CNF |