src/HOL/Nominal/nominal_inductive2.ML

 val inductive_atomize = @{thms induct_atomize};
 val inductive_rulify = @{thms induct_rulify};
 
 fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify [];
 
-val atomize_conv =
+fun atomize_conv ctxt =
   Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
-    (HOL_basic_ss addsimps inductive_atomize);
-val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
+    (put_simpset HOL_basic_ss ctxt addsimps inductive_atomize);
+fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt));
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
-  (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
-
-val fresh_postprocess =
-  Simplifier.full_simplify (HOL_basic_ss addsimps
+  (Conv.params_conv ~1 (K (Conv.prems_conv ~1 (atomize_conv ctxt))) ctxt));
+
+fun fresh_postprocess ctxt =
+  Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps
     [@{thm fresh_star_set_eq}, @{thm fresh_star_Un_elim},
      @{thm fresh_star_insert_elim}, @{thm fresh_star_empty_elim}]);
 
 fun preds_of ps t = inter (op = o apsnd dest_Free) ps (Term.add_frees t []);
 

 
 fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
   [(perm_boolI_pi, pi)] perm_boolI;
 
 fun mk_perm_bool_simproc names = Simplifier.simproc_global_i
-  (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn thy => fn ss =>
+  (theory_of_thm perm_bool) "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
     fn Const ("Nominal.perm", _) $ _ $ t =>
          if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
          then SOME perm_bool else NONE
      | _ => NONE);
 

         SOME (Const ("Fun.id", HOLogic.boolT --> HOLogic.boolT) $
           (subst_bounds (pis, strip_all pis t)))
       else NONE
   | inst_conj_all _ _ _ _ _ = NONE;
 
-fun inst_conj_all_tac k = EVERY
+fun inst_conj_all_tac ctxt k = EVERY
   [TRY (EVERY [etac conjE 1, rtac conjI 1, atac 1]),
    REPEAT_DETERM_N k (etac allE 1),
-   simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1];
+   simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]) 1];
 
 fun map_term f t u = (case f t u of
       NONE => map_term' f t u | x => x)
 and map_term' f (t $ u) (t' $ u') = (case (map_term f t t', map_term f u u') of
       (NONE, NONE) => NONE

       split_list) prems |> split_list;
 
     val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
     val pt2_atoms = map (fn a => Global_Theory.get_thm thy
       ("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
-    val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
+    val eqvt_ss = simpset_of (Simplifier.global_context thy HOL_basic_ss
       addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
       addsimprocs [mk_perm_bool_simproc ["Fun.id"],
-        NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
+        NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
     val fresh_star_bij = Global_Theory.get_thms thy "fresh_star_bij";
     val pt_insts = map (NominalAtoms.pt_inst_of thy) atoms;
     val at_insts = map (NominalAtoms.at_inst_of thy) atoms;
     val dj_thms = maps (fn a =>
       map (NominalAtoms.dj_thm_of thy a) (remove (op =) a atoms)) atoms;

           ("fs_" ^ Long_Name.base_name atom ^ "1");
         val avoid_th = Drule.instantiate'
           [SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)]
           ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
         val (([(_, cx)], th1 :: th2 :: ths), ctxt') = Obtain.result
-          (fn _ => EVERY
+          (fn ctxt' => EVERY
             [rtac avoid_th 1,
-             full_simp_tac (HOL_ss addsimps [@{thm fresh_star_prod_set}]) 1,
-             full_simp_tac (HOL_basic_ss addsimps [@{thm id_apply}]) 1,
+             full_simp_tac (put_simpset HOL_ss ctxt' addsimps [@{thm fresh_star_prod_set}]) 1,
+             full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]) 1,
              rotate_tac 1 1,
              REPEAT (etac conjE 1)])
           [] ctxt;
         val (Ts1, _ :: Ts2) = take_prefix (not o equal T) (map snd sets);
         val pTs = map NominalAtoms.mk_permT (Ts1 @ Ts2);

           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 (HOL_basic_ss addsimps perm_set_forget) 1) |>
-          Simplifier.simplify eqvt_ss
+               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')
       end;
 

       Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
         let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
           rtac raw_induct 1 THEN
           EVERY (maps (fn (((((_, sets, oprems, _),
               vc_compat_ths), vc_compat_vs), ihyp), vs_ihypt) =>
-            [REPEAT (rtac allI 1), simp_tac eqvt_ss 1,
+            [REPEAT (rtac allI 1), simp_tac (put_simpset eqvt_ss context) 1,
              SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
                let
                  val (cparams', (pis, z)) =
                    chop (length params - length atomTs - 1) (map #2 params) ||>
                    (map term_of #> split_last);

                        strip_comb (HOLogic.dest_Trueprop (concl_of th'))
                    in
                      Goal.prove ctxt' [] []
                        (HOLogic.mk_Trueprop (list_comb (h,
                           map (fold_rev (NominalDatatype.mk_perm []) pis) ts)))
-                       (fn _ => simp_tac (HOL_basic_ss addsimps
+                       (fn _ => simp_tac (put_simpset HOL_basic_ss ctxt' addsimps
                           (fresh_star_bij @ finite_ineq)) 1 THEN rtac th' 1)
                    end) vc_compat_ths vc_compat_vs;
                  val (vc_compat_ths1, vc_compat_ths2) =
                    chop (length vc_compat_ths - length sets) vc_compat_ths';
                  val vc_compat_ths1' = map
                    (Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv
-                      (Simplifier.rewrite eqvt_ss)))) vc_compat_ths1;
+                      (Simplifier.rewrite (put_simpset eqvt_ss ctxt'))))) vc_compat_ths1;
                  val (pis', fresh_ths1, fresh_ths2, fresh_ths3, ctxt'') = fold
                    (obtain_fresh_name ts sets)
                    (map snd sets' ~~ vc_compat_ths2) ([], [], [], [], ctxt');
                  fun concat_perm pi1 pi2 =
                    let val T = fastype_of pi1

                  val pis'' = fold_rev (concat_perm #> map) pis' pis;
                  val ihyp' = inst_params thy vs_ihypt ihyp
                    (map (fold_rev (NominalDatatype.mk_perm [])
                       (pis' @ pis) #> cterm_of thy) params' @ [cterm_of thy z]);
                  fun mk_pi th =
-                   Simplifier.simplify (HOL_basic_ss addsimps [@{thm id_apply}]
+                   Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]
                        addsimprocs [NominalDatatype.perm_simproc])
-                     (Simplifier.simplify eqvt_ss
+                     (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 (length pis'')) monos (SOME t) th)))
+                       (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))
                      (fresh_ths2 ~~ sets);
                  val th = Goal.prove ctxt'' [] []
                    (HOLogic.mk_Trueprop (list_comb (P $ hd ts,
                      map (fold_rev (NominalDatatype.mk_perm []) pis') (tl ts))))
-                   (fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1] @
+                   (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1, rtac ihyp' 1] @
                      map (fn th => rtac th 1) fresh_ths3 @
                      [REPEAT_DETERM_N (length gprems)
-                       (simp_tac (HOL_basic_ss
+                       (simp_tac (put_simpset HOL_basic_ss ctxt''
                           addsimps [inductive_forall_def']
                           addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
                         resolve_tac gprems2 1)]));
                  val final = Goal.prove ctxt'' [] [] (term_of concl)
-                   (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss
+                   (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss ctxt''
                      addsimps vc_compat_ths1' @ fresh_ths1 @
                        perm_freshs_freshs') 1);
                  val final' = Proof_Context.export ctxt'' ctxt' [final];
                in resolve_tac final' 1 end) context 1])
                  (prems ~~ thss ~~ vc_compat' ~~ ihyps ~~ prems'')))
         in
           cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
           REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
             etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
-            asm_full_simp_tac (simpset_of ctxt) 1)
+            asm_full_simp_tac ctxt 1)
         end) |>
-        fresh_postprocess |>
+        fresh_postprocess ctxt' |>
         singleton (Proof_Context.export ctxt' ctxt);
 
   in
     ctxt'' |>
     Proof.theorem NONE (fn thss => fn ctxt =>  (* FIXME ctxt/ctxt' should be called lthy/lthy' *)

         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
         val ind_case_names = Rule_Cases.case_names induct_cases;
         val induct_cases' = Inductive.partition_rules' raw_induct
           (intrs ~~ induct_cases); 
-        val thss' = map (map atomize_intr) thss;
+        val thss' = map (map (atomize_intr ctxt)) thss;
         val thsss = Inductive.partition_rules' raw_induct (intrs ~~ thss');
         val strong_raw_induct =
-          mk_ind_proof ctxt thss' |> Inductive.rulify;
+          mk_ind_proof ctxt thss' |> Inductive.rulify ctxt;
         val strong_induct_atts =
           map (Attrib.internal o K)
             [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
         val strong_induct =
           if length names > 1 then strong_raw_induct