--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Nov 19 10:11:11 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Nov 19 14:43:50 2020 +0100
@@ -33,14 +33,14 @@
datatype fool = Without_FOOL | With_FOOL
datatype polymorphism = Monomorphic | Polymorphic
- datatype thf_choice = THF_Without_Choice | THF_With_Choice
+ datatype thf_flavor = THF_Without_Choice | THF_With_Choice
datatype atp_format =
CNF |
CNF_UEQ |
FOF |
TFF of fool * polymorphism |
- THF of fool * polymorphism * thf_choice |
+ THF of fool * polymorphism * thf_flavor |
DFG of polymorphism
datatype atp_formula_role =
@@ -191,14 +191,14 @@
datatype fool = Without_FOOL | With_FOOL
datatype polymorphism = Monomorphic | Polymorphic
-datatype thf_choice = THF_Without_Choice | THF_With_Choice
+datatype thf_flavor = THF_Without_Choice | THF_With_Choice
datatype atp_format =
CNF |
CNF_UEQ |
FOF |
TFF of fool * polymorphism |
- THF of fool * polymorphism * thf_choice |
+ THF of fool * polymorphism * thf_flavor |
DFG of polymorphism
datatype atp_formula_role =
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 19 10:11:11 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 19 14:43:50 2020 +0100
@@ -135,7 +135,7 @@
datatype order =
First_Order |
- Higher_Order of thf_choice
+ Higher_Order of thf_flavor
datatype phantom_policy = Without_Phantom_Type_Vars | With_Phantom_Type_Vars
datatype polymorphism =
Type_Class_Polymorphic |