diff -r 780b7a2c50b6 -r 35bb5b013f0e Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Sun Dec 15 15:14:40 2013 +1100
+++ b/Nominal/nominal_function_core.ML	Sat Jan 11 23:17:23 2014 +0000
@@ -485,7 +485,8 @@
     val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
 
     val ih_intro_case =
-      full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp]) ih_intro
+      full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp])
+        ih_intro
 
     fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = 
         (llRI RS ih_intro_case)
@@ -519,7 +520,8 @@
       ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
       |> curry (op COMP) existence
       |> curry (op COMP) uniqueness
-      |> simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp RS sym])
+      |> simplify
+          (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp RS sym])
       |> Thm.implies_intr (cprop_of case_hyp)
       |> fold_rev (Thm.implies_intr o cprop_of) ags
       |> fold_rev Thm.forall_intr cqs
@@ -734,7 +736,7 @@
         |> Thm.forall_intr (cterm_of thy z)
         |> (fn it => it COMP valthm)
         |> Thm.implies_intr lhs_acc
-        |> asm_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [f_iff])
+        |> asm_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [f_iff])
         |> fold_rev (Thm.implies_intr o cprop_of) ags
         |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
       end
@@ -889,7 +891,8 @@
       qglr=(oqs, _, _, _), ...} = clause
 
     val ih_case =
-      full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [case_hyp]) ihyp
+      full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [case_hyp])
+        ihyp
 
     fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
       let
@@ -979,7 +982,7 @@
     |> Thm.forall_intr (cterm_of thy R')
     |> Thm.forall_elim (cterm_of thy (inrel_R))
     |> curry op RS wf_in_rel
-    |> full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [in_rel_def])
+    |> full_simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps [in_rel_def])
     |> Thm.forall_intr (cterm_of thy Rrel)
   end