# HG changeset patch
# User wenzelm
# Date 1368356903 -7200
# Node ID db22d73e6c3e8774df95a290afa31f1bbe9afadc
# Parent  972c4f42fd525857369c89fd1938321e8397abb3
proper context;

diff -r 972c4f42fd52 -r db22d73e6c3e src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Sat May 11 22:20:59 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Sun May 12 13:08:23 2013 +0200
@@ -107,15 +107,13 @@
   (rtac uexhaust THEN'
    EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases)) 1;
 
-val naked_ctxt = @{theory_context HOL};
-
 (* TODO: More precise "simp_thms"; get rid of "blast_tac" *)
 fun mk_split_tac ctxt uexhaust cases injectss distinctsss =
   rtac uexhaust 1 THEN
   ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
      simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @
        flat (nth distinctsss (k - 1))) ctxt)) k) THEN
-  ALLGOALS (blast_tac naked_ctxt);
+  ALLGOALS (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt));
 
 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};