--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 13 09:58:08 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 13 10:26:56 2013 +0200
@@ -30,7 +30,6 @@
gen_simp : bool}
datatype polymorphism = Monomorphic | Polymorphic
- datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_choice = THF_Without_Choice | THF_With_Choice
datatype thf_defs = THF_Without_Defs | THF_With_Defs
@@ -38,8 +37,8 @@
CNF |
CNF_UEQ |
FOF |
- TFF of polymorphism * tptp_explicitness |
- THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
+ TFF of polymorphism |
+ THF of polymorphism * thf_choice * thf_defs |
DFG of polymorphism
datatype formula_role =
@@ -175,7 +174,6 @@
gen_simp : bool}
datatype polymorphism = Monomorphic | Polymorphic
-datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit
datatype thf_choice = THF_Without_Choice | THF_With_Choice
datatype thf_defs = THF_Without_Defs | THF_With_Defs
@@ -183,8 +181,8 @@
CNF |
CNF_UEQ |
FOF |
- TFF of polymorphism * tptp_explicitness |
- THF of polymorphism * tptp_explicitness * thf_choice * thf_defs |
+ TFF of polymorphism |
+ THF of polymorphism * thf_choice * thf_defs |
DFG of polymorphism
datatype formula_role =
@@ -911,7 +909,7 @@
if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
val avoid_clash =
case format of
- TFF (Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars
+ TFF Polymorphic => avoid_clash_with_alt_ergo_type_vars
| DFG _ => avoid_clash_with_dfg_keywords
| _ => I
val nice_name = nice_name avoid_clash