# HG changeset patch
# User desharna
# Date 1605793430 -3600
# Node ID febfb98d09418c00d048598428fb49066804c29b
# Parent  a17c17ab931ca11fb976a38cc58abfa0d5cd902f
renamed data type

diff -r a17c17ab931c -r febfb98d0941 src/HOL/Tools/ATP/atp_problem.ML
--- 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 =
diff -r a17c17ab931c -r febfb98d0941 src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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 |