Changed Simplifier.simp_modifiers to Simplifier.simp_modifiers'.
This means the syntax of the tactics supports_simp and perm_simp
are exactly like simp, namely

(supports_simp add: .... del: ...)

where the add's and del's are optional.

--- a/src/HOL/Nominal/nominal_permeq.ML	Sat Oct 29 14:37:32 2005 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Sat Oct 29 15:01:25 2005 +0200
@@ -110,7 +110,7 @@
 
 
 fun simp_meth_setup tac =
-  Method.only_sectioned_args (Simplifier.simp_modifiers @ Splitter.split_modifiers)
+  Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
   (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
 
 val perm_eq_meth        = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);