src/HOL/Nominal/nominal_fresh_fun.ML
changeset 51717 9e7d1c139569
parent 51669 7fbc4fc400d8
child 55951 c07d184aebe9
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -129,9 +129,9 @@
     1.4      val thy = theory_of_thm thm;
     1.5      val abs_fresh = Global_Theory.get_thms thy "abs_fresh";
     1.6      val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
     1.7 -    val ss = simpset_of ctxt;
     1.8 -    val ss' = ss addsimps fresh_prod::abs_fresh;
     1.9 -    val ss'' = ss' addsimps fresh_perm_app;
    1.10 +    val simp_ctxt =
    1.11 +      ctxt addsimps (fresh_prod :: abs_fresh)
    1.12 +      addsimps fresh_perm_app;
    1.13      val x = hd (tl (Misc_Legacy.term_vars (prop_of exI)));
    1.14      val goal = nth (prems_of thm) (i-1);
    1.15      val atom_name_opt = get_inner_fresh_fun goal;
    1.16 @@ -164,10 +164,10 @@
    1.17      val post_rewrite_tacs =
    1.18            [rtac pt_name_inst,
    1.19             rtac at_name_inst,
    1.20 -           TRY o SOLVED' (NominalPermeq.finite_guess_tac ss''),
    1.21 +           TRY o SOLVED' (NominalPermeq.finite_guess_tac simp_ctxt),
    1.22             inst_fresh vars params THEN'
    1.23 -           (TRY o SOLVED' (NominalPermeq.fresh_guess_tac ss'')) THEN'
    1.24 -           (TRY o SOLVED' (asm_full_simp_tac ss''))]
    1.25 +           (TRY o SOLVED' (NominalPermeq.fresh_guess_tac simp_ctxt)) THEN'
    1.26 +           (TRY o SOLVED' (asm_full_simp_tac simp_ctxt))]
    1.27    in
    1.28     ((if no_asm then no_tac else
    1.29      (subst_inner_asm_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i)))