src/HOL/Nominal/nominal_permeq.ML

               in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
             else NONE)
       | _ => NONE
   end
 
-val perm_simproc_app = Simplifier.simproc @{theory} "perm_simproc_app"
+val perm_simproc_app = Simplifier.simproc_global @{theory} "perm_simproc_app"
   ["Nominal.perm pi x"] perm_simproc_app';
 
 (* a simproc that deals with permutation instances in front of functions  *)
 fun perm_simproc_fun' sg ss redex = 
    let 

        (Const("Nominal.perm",_) $ pi $ f)  => 
           (if (applicable_fun f) then SOME (perm_fun_def) else NONE)
       | _ => NONE
    end
 
-val perm_simproc_fun = Simplifier.simproc @{theory} "perm_simproc_fun"
+val perm_simproc_fun = Simplifier.simproc_global @{theory} "perm_simproc_fun"
   ["Nominal.perm pi x"] perm_simproc_fun';
 
 (* function for simplyfying permutations          *)
 (* stac contains the simplifiation tactic that is *)
 (* applied (see (no_asm) options below            *)

              cp1_aux)))
       else NONE
     end
   | _ => NONE);
 
-val perm_compose_simproc = Simplifier.simproc @{theory} "perm_compose"
+val perm_compose_simproc = Simplifier.simproc_global @{theory} "perm_compose"
   ["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc';
 
 fun perm_compose_tac ss i = 
   ("analysing permutation compositions on the lhs",
    fn st => EVERY