more accurate context;
authorwenzelm
Fri Jan 10 17:44:41 2014 +0100 (2014-01-10)
changeset 549832c57fc1f7a8c
parent 54982 b327bf0dabfb
child 54984 da70ab8531f4
more accurate context;
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Jan 10 16:55:37 2014 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Jan 10 17:44:41 2014 +0100
     1.3 @@ -343,19 +343,19 @@
     1.4                      map (fold_rev (NominalDatatype.mk_perm [])
     1.5                        (rev pis' @ pis)) params' @ [z])) ihyp;
     1.6                   fun mk_pi th =
     1.7 -                   Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]
     1.8 +                   Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
     1.9                         addsimprocs [NominalDatatype.perm_simproc])
    1.10 -                     (Simplifier.simplify (put_simpset eqvt_ss ctxt)
    1.11 +                     (Simplifier.simplify (put_simpset eqvt_ss ctxt')
    1.12                         (fold_rev (mk_perm_bool o cterm_of thy)
    1.13                           (rev pis' @ pis) th));
    1.14                   val (gprems1, gprems2) = split_list
    1.15                     (map (fn (th, t) =>
    1.16                        if null (preds_of ps t) then (SOME th, mk_pi th)
    1.17                        else
    1.18 -                        (map_thm ctxt (split_conj (K o I) names)
    1.19 +                        (map_thm ctxt' (split_conj (K o I) names)
    1.20                             (etac conjunct1 1) monos NONE th,
    1.21 -                         mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
    1.22 -                           (inst_conj_all_tac ctxt (length pis'')) monos (SOME t) th))))
    1.23 +                         mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis''))
    1.24 +                           (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th))))
    1.25                        (gprems ~~ oprems)) |>> map_filter I;
    1.26                   val vc_compat_ths' = map (fn th =>
    1.27                     let
    1.28 @@ -625,9 +625,9 @@
    1.29            in error ("Could not prove equivariance for introduction rule\n" ^
    1.30              Syntax.string_of_term ctxt''' t ^ "\n" ^ s)
    1.31            end;
    1.32 -        val res = SUBPROOF (fn {prems, params, ...} =>
    1.33 +        val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} =>
    1.34            let
    1.35 -            val prems' = map (fn th => the_default th (map_thm ctxt'
    1.36 +            val prems' = map (fn th => the_default th (map_thm ctxt''
    1.37                (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;
    1.38              val prems'' = map (fn th => Simplifier.simplify eqvt_simpset
    1.39                (mk_perm_bool (cterm_of thy pi) th)) prems';
     2.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Jan 10 16:55:37 2014 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Jan 10 17:44:41 2014 +0100
     2.3 @@ -335,13 +335,13 @@
     2.4            (map Bound (length pTs - 1 downto 0));
     2.5          val _ $ (f $ (_ $ pi $ l) $ r) = prop_of th2
     2.6          val th2' =
     2.7 -          Goal.prove ctxt [] []
     2.8 +          Goal.prove ctxt' [] []
     2.9              (Logic.list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop
    2.10                 (f $ fold_rev (NominalDatatype.mk_perm (rev pTs))
    2.11                    (pis1 @ pi :: pis2) l $ r)))
    2.12              (fn _ => cut_facts_tac [th2] 1 THEN
    2.13 -               full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps perm_set_forget) 1) |>
    2.14 -          Simplifier.simplify (put_simpset eqvt_ss ctxt)
    2.15 +               full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps perm_set_forget) 1) |>
    2.16 +          Simplifier.simplify (put_simpset eqvt_ss ctxt')
    2.17        in
    2.18          (freshs @ [term_of cx],
    2.19           ths1 @ ths, ths2 @ [th1], ths3 @ [th2'], ctxt')
    2.20 @@ -401,16 +401,16 @@
    2.21                     (map (fold_rev (NominalDatatype.mk_perm [])
    2.22                        (pis' @ pis) #> cterm_of thy) params' @ [cterm_of thy z]);
    2.23                   fun mk_pi th =
    2.24 -                   Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]
    2.25 +                   Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
    2.26                         addsimprocs [NominalDatatype.perm_simproc])
    2.27 -                     (Simplifier.simplify (put_simpset eqvt_ss ctxt)
    2.28 +                     (Simplifier.simplify (put_simpset eqvt_ss ctxt')
    2.29                         (fold_rev (mk_perm_bool o cterm_of thy)
    2.30                           (pis' @ pis) th));
    2.31                   val gprems2 = map (fn (th, t) =>
    2.32                     if null (preds_of ps t) then mk_pi th
    2.33                     else
    2.34 -                     mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
    2.35 -                       (inst_conj_all_tac ctxt (length pis'')) monos (SOME t) th)))
    2.36 +                     mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis''))
    2.37 +                       (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th)))
    2.38                     (gprems ~~ oprems);
    2.39                   val perm_freshs_freshs' = map (fn (th, (_, T)) =>
    2.40                     th RS the (AList.lookup op = perm_freshs_freshs T))