# HG changeset patch
# User blanchet
# Date 1482338278 -3600
# Node ID a331208010b61a04b7879ffcfd46e5791f38e310
# Parent  19bc22274cd9490ceb496953fc2d17aa0e4c98c3
moved and exported tactic

diff -r 19bc22274cd9 -r a331208010b6 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- 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;
diff -r 19bc22274cd9 -r a331208010b6 src/HOL/Tools/BNF/bnf_tactics.ML
--- 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];