Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use proper context in function
authordesharna
Fri, 19 Dec 2014 11:20:07 +0100
changeset 59274 67afe7e6a516
parent 59273 2c1e58190664
child 59275 77cd4992edcd
use proper context in function
src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle