--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Dec 21 13:35:58 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Dec 21 17:37:58 2016 +0100
@@ -37,8 +37,6 @@
val split_connectI = @{thms allI impI conjI};
val unfold_lets = @{thms Let_def[abs_def] split_beta}
-fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
-
fun exhaust_inst_as_projs ctxt frees thm =
let
val num_frees = length frees;
--- a/src/HOL/Tools/BNF/bnf_tactics.ML Wed Dec 21 13:35:58 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML Wed Dec 21 17:37:58 2016 +0100
@@ -11,6 +11,7 @@
include CTR_SUGAR_GENERAL_TACTICS
val fo_rtac: Proof.context -> thm -> int -> tactic
+ val clean_blast_tac: Proof.context -> int -> tactic
val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic
val subst_asm_tac: Proof.context -> int list option -> thm list -> int -> tactic
@@ -43,6 +44,8 @@
end
handle Pattern.MATCH => no_tac) ctxt;
+fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
+
(*unlike "unfold_thms_tac", it succeed when the RHS contains schematic variables not in the LHS*)
fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];
fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt o the_default [0];