--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 28 16:58:27 2014 +0200
@@ -137,7 +137,7 @@
basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @
[Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)]
val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods
-val skolem_methods = basic_systematic_methods @ [Skolem_Method]
+fun skolem_methods_of z3 = (basic_systematic_methods, [Skolem_Method]) |> z3 ? swap |> op @
fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
(one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
@@ -185,9 +185,12 @@
fun add_lemma ((l, t), rule) ctxt =
let
val (skos, meths) =
- (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods)
- else if is_arith_rule rule then ([], arith_methods)
- else ([], rewrite_methods))
+ (if is_skolemize_rule rule then
+ (skolems_of ctxt t, skolem_methods_of (rule = z3_skolemize_rule))
+ else if is_arith_rule rule then
+ ([], arith_methods)
+ else
+ ([], rewrite_methods))
||> massage_methods
in
(Prove ([], skos, l, t, [], ([], []), meths, ""),
@@ -260,7 +263,7 @@
|> fold add_fact_of_dependencies gamma
|> sort_facts
val meths =
- (if skolem then skolem_methods
+ (if skolem then skolem_methods_of (rule = z3_skolemize_rule)
else if is_arith_rule rule then arith_methods
else if is_datatype_rule rule then datatype_methods
else systematic_methods')