--- a/src/HOL/Nominal/nominal_datatype.ML Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Feb 19 16:11:45 2010 +0100
@@ -1547,7 +1547,7 @@
(augment_sort thy1 pt_cp_sort
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
(fn _ => rtac rec_induct 1 THEN REPEAT
- (simp_tac (Simplifier.theory_context thy11 HOL_basic_ss
+ (simp_tac (Simplifier.global_context thy11 HOL_basic_ss
addsimps flat perm_simps'
addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
(resolve_tac rec_intrs THEN_ALL_NEW
@@ -1951,7 +1951,7 @@
(HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs'))
(fn _ => EVERY
[cut_facts_tac [th'] 1,
- full_simp_tac (Simplifier.theory_context thy11 HOL_ss
+ full_simp_tac (Simplifier.global_context thy11 HOL_ss
addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
addsimprocs [NominalPermeq.perm_simproc_app]) 1,
full_simp_tac (HOL_ss addsimps (calc_atm @