--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Thu Jan 02 09:50:22 2014 +0100
@@ -7,6 +7,7 @@
signature CTR_SUGAR_GENERAL_TACTICS =
sig
+ val clean_blast_tac: Proof.context -> int -> tactic
val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
val unfold_thms_tac: Proof.context -> thm list -> tactic
end;
@@ -41,6 +42,8 @@
val meta_mp = @{thm meta_mp};
+fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
+
fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
@@ -157,7 +160,7 @@
ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
flat (nth distinctsss (k - 1))) ctxt)) k) THEN
- ALLGOALS (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt));
+ ALLGOALS (clean_blast_tac ctxt);
val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};