--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 16:07:34 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 19:32:10 2014 +0200
@@ -47,7 +47,7 @@
val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
val e_skolemize_rule = "skolemize"
-val leo2_extcnf_combined_rule = "extcnf_combined"
+val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg"
val satallax_skolemize_rule = "tab_ex"
val spass_pirate_datatype_rule = "DT"
val vampire_skolemisation_rule = "skolemisation"
@@ -61,10 +61,8 @@
val z3_th_lemma_rule = "th-lemma"
val zipperposition_cnf_rule = "cnf"
-(* Unfortunately, LEO-II's "extcnf_combined" rule captures clausification in general and not only
- skolemization. *)
val skolemize_rules =
- [e_skolemize_rule, leo2_extcnf_combined_rule, satallax_skolemize_rule, spass_skolemize_rule,
+ [e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, spass_skolemize_rule,
vampire_skolemisation_rule, veriT_tmp_ite_elim_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule,
zipperposition_cnf_rule]