src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
changeset 60251 98754695b421
parent 59621 291934bac95e
child 60728 26ffdb966759
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun May 03 20:21:25 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Sun May 03 18:14:11 2015 +0200
     1.3 @@ -37,6 +37,8 @@
     1.4  val split_connectI = @{thms allI impI conjI};
     1.5  val unfold_lets = @{thms Let_def[abs_def] split_beta}
     1.6  
     1.7 +fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt);
     1.8 +
     1.9  fun exhaust_inst_as_projs ctxt frees thm =
    1.10    let
    1.11      val num_frees = length frees;