# HG changeset patch
# User wenzelm
# Date 1389372281 -3600
# Node ID 2c57fc1f7a8c0d3917b9047362e3f0785c748771
# Parent  b327bf0dabfb3426e229ae077245d03bc9c47495
more accurate context;

diff -r b327bf0dabfb -r 2c57fc1f7a8c src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Jan 10 16:55:37 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Jan 10 17:44:41 2014 +0100
@@ -343,19 +343,19 @@
                     map (fold_rev (NominalDatatype.mk_perm [])
                       (rev pis' @ pis)) params' @ [z])) ihyp;
                  fun mk_pi th =
-                   Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]
+                   Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
                        addsimprocs [NominalDatatype.perm_simproc])
-                     (Simplifier.simplify (put_simpset eqvt_ss ctxt)
+                     (Simplifier.simplify (put_simpset eqvt_ss ctxt')
                        (fold_rev (mk_perm_bool o cterm_of thy)
                          (rev pis' @ pis) th));
                  val (gprems1, gprems2) = split_list
                    (map (fn (th, t) =>
                       if null (preds_of ps t) then (SOME th, mk_pi th)
                       else
-                        (map_thm ctxt (split_conj (K o I) names)
+                        (map_thm ctxt' (split_conj (K o I) names)
                            (etac conjunct1 1) monos NONE th,
-                         mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
-                           (inst_conj_all_tac ctxt (length pis'')) monos (SOME t) th))))
+                         mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis''))
+                           (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th))))
                       (gprems ~~ oprems)) |>> map_filter I;
                  val vc_compat_ths' = map (fn th =>
                    let
@@ -625,9 +625,9 @@
           in error ("Could not prove equivariance for introduction rule\n" ^
             Syntax.string_of_term ctxt''' t ^ "\n" ^ s)
           end;
-        val res = SUBPROOF (fn {prems, params, ...} =>
+        val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} =>
           let
-            val prems' = map (fn th => the_default th (map_thm ctxt'
+            val prems' = map (fn th => the_default th (map_thm ctxt''
               (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;
             val prems'' = map (fn th => Simplifier.simplify eqvt_simpset
               (mk_perm_bool (cterm_of thy pi) th)) prems';
diff -r b327bf0dabfb -r 2c57fc1f7a8c src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Jan 10 16:55:37 2014 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Jan 10 17:44:41 2014 +0100
@@ -335,13 +335,13 @@
           (map Bound (length pTs - 1 downto 0));
         val _ $ (f $ (_ $ pi $ l) $ r) = prop_of th2
         val th2' =
-          Goal.prove ctxt [] []
+          Goal.prove ctxt' [] []
             (Logic.list_all (map (pair "pi") pTs, HOLogic.mk_Trueprop
                (f $ fold_rev (NominalDatatype.mk_perm (rev pTs))
                   (pis1 @ pi :: pis2) l $ r)))
             (fn _ => cut_facts_tac [th2] 1 THEN
-               full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps perm_set_forget) 1) |>
-          Simplifier.simplify (put_simpset eqvt_ss ctxt)
+               full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps perm_set_forget) 1) |>
+          Simplifier.simplify (put_simpset eqvt_ss ctxt')
       in
         (freshs @ [term_of cx],
          ths1 @ ths, ths2 @ [th1], ths3 @ [th2'], ctxt')
@@ -401,16 +401,16 @@
                    (map (fold_rev (NominalDatatype.mk_perm [])
                       (pis' @ pis) #> cterm_of thy) params' @ [cterm_of thy z]);
                  fun mk_pi th =
-                   Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]
+                   Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
                        addsimprocs [NominalDatatype.perm_simproc])
-                     (Simplifier.simplify (put_simpset eqvt_ss ctxt)
+                     (Simplifier.simplify (put_simpset eqvt_ss ctxt')
                        (fold_rev (mk_perm_bool o cterm_of thy)
                          (pis' @ pis) th));
                  val gprems2 = map (fn (th, t) =>
                    if null (preds_of ps t) then mk_pi th
                    else
-                     mk_pi (the (map_thm ctxt (inst_conj_all names ps (rev pis''))
-                       (inst_conj_all_tac ctxt (length pis'')) monos (SOME t) th)))
+                     mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis''))
+                       (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th)))
                    (gprems ~~ oprems);
                  val perm_freshs_freshs' = map (fn (th, (_, T)) =>
                    th RS the (AList.lookup op = perm_freshs_freshs T))