# HG changeset patch
# User fleury
# Date 1406721793 -7200
# Node ID cf8e4b1acd33eb8e81473aee8f5b75083f832c30
# Parent  4856a7b8b9c3e2f0844939a19793acef4f46b74b
Skolemization for tmp_ite_elim rule in the SMT solver veriT.

diff -r 4856a7b8b9c3 -r cf8e4b1acd33 src/HOL/Tools/SMT2/verit_proof.ML
--- a/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -303,7 +303,7 @@
       let
         val concl' = replace_bound_var_by_free_var concl bounds
       in
-        mk_node id veriT_tmp_skolemize_rule prems concl' []
+        mk_node id rule prems concl' []
       end
   else
     st
diff -r 4856a7b8b9c3 -r cf8e4b1acd33 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:13 2014 +0200
@@ -52,6 +52,8 @@
 val spass_pirate_datatype_rule = "DT"
 val vampire_skolemisation_rule = "skolemisation"
 val veriT_tmp_skolemize_rule = "tmp_skolemize"
+val veriT_tmp_ite_elim_rule = "tmp_ite_elim"
+val veriT_skolemize_rules = [veriT_tmp_ite_elim_rule, veriT_tmp_skolemize_rule]
 val veriT_simp_arith_rule = "simp_arith"
 val veriT_la_generic_rule = "la_generic"
 val veriT_arith_rules = [veriT_simp_arith_rule, veriT_la_generic_rule]
@@ -62,8 +64,7 @@
 
 val skolemize_rules =
   [e_skolemize_rule, leo2_extcnf_combined_rule, satallax_skolemize_rule, spass_skolemize_rule,
-    vampire_skolemisation_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule,
-    zipperposition_cnf_rule]
+    vampire_skolemisation_rule, z3_skolemize_rule, zipperposition_cnf_rule] @ veriT_skolemize_rules
 
 val is_skolemize_rule = member (op =) skolemize_rules
 val is_arith_rule = String.isPrefix z3_th_lemma_rule orf member (op =) veriT_arith_rules