diff -r ee0881a54c72 -r 3d6ac2f68bf3 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 16 17:18:52 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 16 17:58:31 2013 +0100
@@ -46,7 +46,7 @@
 
 open String_Redirect
 
-val e_skolemize_rule = "skolemize"
+val e_skolemize_rules = ["skolemize", "shift_quantors"]
 val vampire_skolemisation_rule = "skolemisation"
 (* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
 val z3_apply_def_rule = "apply-def"
@@ -56,9 +56,9 @@
 val z3_skolemize_rule = "sk"
 val z3_th_lemma_rule = "th-lemma"
 
-val is_skolemize_rule =
-  member (op =) [e_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
+val skolemize_rules = e_skolemize_rules @ [vampire_skolemisation_rule, z3_skolemize_rule]
 
+val is_skolemize_rule = member (op =) skolemize_rules
 val is_arith_rule = String.isPrefix z3_th_lemma_rule
 
 fun raw_label_of_num num = (num, 0)