# HG changeset patch
# User desharna
# Date 1418984407 -3600
# Node ID 67afe7e6a5163ec7083b0d7abfef0ea2165abc3c
# Parent  2c1e581906640119851b0ced545da45dfd34112b
use proper context in function

diff -r 2c1e58190664 -r 67afe7e6a516 src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- 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