--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 14:03:11 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 14:03:12 2014 +0200
@@ -57,7 +57,7 @@
val skolemize_rules =
[e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule,
-zipperposition_cnf_rule, leo2_extcnf_combined_rule]
+zipperposition_cnf_rule, leo2_extcnf_combined_rule, veriT_skomelisation_rule]
val is_skolemize_rule = member (op =) skolemize_rules
val is_arith_rule = String.isPrefix z3_th_lemma_rule