--- a/src/HOL/Nominal/nominal_permeq.ML Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Fri Feb 19 16:11:45 2010 +0100
@@ -143,7 +143,7 @@
fun perm_simp_gen stac dyn_thms eqvt_thms ss i =
("general simplification of permutations", fn st =>
let
- val ss' = Simplifier.theory_context (theory_of_thm st) ss
+ val ss' = Simplifier.global_context (theory_of_thm st) ss
addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
delcongs weak_congs
addcongs strong_congs
@@ -221,7 +221,7 @@
("analysing permutation compositions on the lhs",
fn st => EVERY
[rtac trans i,
- asm_full_simp_tac (Simplifier.theory_context (theory_of_thm st) empty_ss
+ asm_full_simp_tac (Simplifier.global_context (theory_of_thm st) empty_ss
addsimprocs [perm_compose_simproc]) i,
asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i] st);