# HG changeset patch
# User blanchet
# Date 1406220398 -7200
# Node ID f89c0749533d58eb72eb669f8f284a6a7eb65438
# Parent  4b247a7586c92324bf4746a3ad760822129f2135
'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)

diff -r 4b247a7586c9 -r f89c0749533d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 24 17:58:29 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 24 18:46:38 2014 +0200
@@ -46,7 +46,7 @@
 
 val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
 
-val e_skolemize_rules = ["skolemize", "shift_quantors"]
+val e_skolemize_rule = "skolemize"
 val spass_pirate_datatype_rule = "DT"
 val vampire_skolemisation_rule = "skolemisation"
 (* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
@@ -54,7 +54,7 @@
 val z3_th_lemma_rule = "th-lemma"
 
 val skolemize_rules =
-  e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
+  [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
 
 val is_skolemize_rule = member (op =) skolemize_rules
 val is_arith_rule = String.isPrefix z3_th_lemma_rule