--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Oct 30 16:24:01 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Oct 30 16:24:04 2018 +0100
@@ -55,7 +55,6 @@
val vampire_skolemisation_rule = "skolemisation"
val veriT_la_generic_rule = "la_generic"
val veriT_simp_arith_rule = "simp_arith"
-val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
val veriT_tmp_skolemize_rule = "tmp_skolemize"
val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize
val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "")
@@ -63,7 +62,7 @@
val skolemize_rules =
[e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
- spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_ite_elim_rule,
+ spass_skolemize_rule, vampire_skolemisation_rule,
veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule]
fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule)