src/HOL/Nominal/nominal_permeq.ML

--- a/src/HOL/Nominal/nominal_permeq.ML	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Sep 17 21:27:08 2008 +0200
@@ -118,7 +118,7 @@
       | _ => NONE
   end
 
-val perm_simproc_app = Simplifier.simproc @{theory} "perm_simproc_app"
+val perm_simproc_app = Simplifier.simproc (the_context ()) "perm_simproc_app"
   ["Nominal.perm pi x"] perm_simproc_app';
 
 (* a simproc that deals with permutation instances in front of functions  *)
@@ -138,7 +138,7 @@
       | _ => NONE
    end
 
-val perm_simproc_fun = Simplifier.simproc @{theory} "perm_simproc_fun"
+val perm_simproc_fun = Simplifier.simproc (the_context ()) "perm_simproc_fun"
   ["Nominal.perm pi x"] perm_simproc_fun';
 
 (* function for simplyfying permutations *)
@@ -210,7 +210,7 @@
     end
   | _ => NONE);
 
-val perm_compose_simproc = Simplifier.simproc @{theory} "perm_compose"
+val perm_compose_simproc = Simplifier.simproc (the_context ()) "perm_compose"
   ["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc';
 
 fun perm_compose_tac ss i =