src/HOL/Nominal/nominal_datatype.ML

         val ths = map (fn th => Drule.export_without_context (th RS mp)) (Datatype_Aux.split_conj_thm
           (Goal.prove_global_future thy11 [] []
             (augment_sort thy1 pt_cp_sort
               (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
             (fn {context = ctxt, ...} => rtac rec_induct 1 THEN REPEAT
-               (simp_tac (Simplifier.global_context thy11 HOL_basic_ss
+               (simp_tac (put_simpset HOL_basic_ss ctxt
                   addsimps flat perm_simps'
                   addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
                 (resolve_tac rec_intrs THEN_ALL_NEW
                  asm_simp_tac (put_simpset HOL_ss ctxt addsimps (fresh_bij @ perm_bij))) 1))))
         val ths' = map (fn ((P, Q), th) =>

                         (fn _ => simp_tac (put_simpset HOL_ss context'' addsimps fresh_bij) 1 THEN
                            rtac th 1)
                       in
                         Goal.prove context'' [] []
                           (HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs'))
-                          (fn _ => EVERY
+                          (fn {context = ctxt, ...} => EVERY
                              [cut_facts_tac [th'] 1,
-                              full_simp_tac (Simplifier.global_context thy11 HOL_ss  (* FIXME context'' (!?) *)
+                              full_simp_tac (put_simpset HOL_ss ctxt
                                 addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
                                 addsimprocs [NominalPermeq.perm_simproc_app]) 1,
                               full_simp_tac (put_simpset HOL_ss context'' addsimps (calc_atm @
                                 fresh_prems' @ freshs2' @ perm_fresh_fresh)) 1])
                       end;