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;