# HG changeset patch
# User blanchet
# Date 1387213111 -3600
# Node ID 3d6ac2f68bf329c7a30910cdec9648a5280e2cd7
# Parent  ee0881a54c72d96ce1681e65391fdc0399c2bd23
correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference

diff -r ee0881a54c72 -r 3d6ac2f68bf3 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Dec 16 17:18:52 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Dec 16 17:58:31 2013 +0100
@@ -231,8 +231,7 @@
 val dummy_phi = AAtom (ATerm (("", []), []))
 val dummy_inference = Inference_Source ("", [])
 
-(* "skip_term" is there to cope with Waldmeister nonsense such as
-   "theory(equality)". *)
+(* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *)
 fun parse_dependency x =
   (parse_inference_source >> snd
    || scan_general_id --| skip_term >> single) x
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)