# HG changeset patch
# User urbanc
# Date 1130590885 -7200
# Node ID b7389981170b657c32a0bf42520ed4c447228acb
# Parent  6d69a4190eb2f66a5710ef584b046a346a72093d
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.

diff -r 6d69a4190eb2 -r b7389981170b src/HOL/Nominal/nominal_permeq.ML
--- 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);