--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Dec 19 11:19:14 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Dec 19 11:20:07 2014 +0100
@@ -80,9 +80,9 @@
etac notE THEN' atac ORELSE'
etac disjE))));
-val ss_fst_snd_conv = simpset_of (ss_only @{thms fst_conv snd_conv} @{context});
+fun ss_fst_snd_conv ctxt = simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
-fun case_atac ctxt = simp_tac (put_simpset ss_fst_snd_conv ctxt);
+fun case_atac ctxt = simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
fun same_case_tac ctxt m =
HEADGOAL (if m = 0 then rtac TrueI