1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 24 17:58:29 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 24 18:46:38 2014 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4  
     1.5  val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
     1.6  
     1.7 -val e_skolemize_rules = ["skolemize", "shift_quantors"]
     1.8 +val e_skolemize_rule = "skolemize"
     1.9  val spass_pirate_datatype_rule = "DT"
    1.10  val vampire_skolemisation_rule = "skolemisation"
    1.11  (* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
    1.12 @@ -54,7 +54,7 @@
    1.13  val z3_th_lemma_rule = "th-lemma"
    1.14  
    1.15  val skolemize_rules =
    1.16 -  e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
    1.17 +  [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
    1.18  
    1.19  val is_skolemize_rule = member (op =) skolemize_rules
    1.20  val is_arith_rule = String.isPrefix z3_th_lemma_rule