src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML

     resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
     dresolve_tac discIs THEN' atac ORELSE'
     etac notE THEN' atac ORELSE'
     etac disjE))));
 
-val ss_fst_snd_conv = simpset_of (ss_only @{thms fst_conv snd_conv} @{context});
-
-fun case_atac ctxt = simp_tac (put_simpset ss_fst_snd_conv ctxt);
+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) ctxt);
 
 fun same_case_tac ctxt m =
   HEADGOAL (if m = 0 then rtac TrueI
     else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' case_atac ctxt) THEN' case_atac ctxt);