src/HOL/Nominal/nominal_inductive.ML
changeset 54983 2c57fc1f7a8c
parent 54895 515630483010
child 54991 1169c65e9698
     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';