src/HOL/Nominal/nominal_datatype.ML

       fold (fn atom => fn thy =>
         let val pt_name = pt_class_of thy atom
         in
           fold (fn (s, tvs) => fn thy => Axclass.prove_arity
               (s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name])
-              (fn _ => EVERY
+              (fn ctxt => EVERY
                 [Class.intro_classes_tac [],
                  resolve_tac perm_empty_thms 1,
                  resolve_tac perm_append_thms 1,
-                 resolve_tac perm_eq_thms 1, assume_tac 1]) thy)
+                 resolve_tac perm_eq_thms 1, assume_tac ctxt 1]) thy)
             (full_new_type_names' ~~ tyvars) thy
         end) atoms |>
       Global_Theory.add_thmss
         [((Binding.name (space_implode "_" new_type_names ^ "_unfolded_perm_eq"),
           unfolded_perm_eq_thms), [Simplifier.simp_add]),

                end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))))
         (fn {context = ctxt, ...} => EVERY
            [Old_Datatype_Aux.ind_tac rep_induct [] 1,
             ALLGOALS (simp_tac (ctxt addsimps
               (Thm.symmetric perm_fun_def :: abs_perm))),
-            ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
+            ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac ctxt)])),
         length new_type_names));
 
     val perm_closed_thmss = map mk_perm_closed atoms;
 
     (**** typedef ****)

                  (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
                     (map (fn (((x, y), S), P) => HOLogic.mk_imp
                       (S $ Free x $ Free y, P $ (Free y)))
                         (rec_unique_frees'' ~~ rec_unique_frees' ~~
                            rec_sets ~~ rec_preds)))))
-               (fn _ =>
+               (fn {context = ctxt, ...} =>
                   rtac rec_induct 1 THEN
-                  REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac) 1))));
+                  REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac ctxt) 1))));
            val rec_fin_supp_thms' = map
              (fn (ths, (T, fin_ths)) => (T, map (curry op MRS fin_ths) ths))
              (rec_fin_supp_thms ~~ finite_thss);
          in EVERY
            ([rtac induct_aux_rec 1] @