--- a/src/HOL/Nominal/nominal_permeq.ML Wed Nov 29 15:44:46 2006 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Wed Nov 29 15:44:51 2006 +0100
@@ -332,7 +332,7 @@
fun simp_meth_setup tac =
Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
- (Method.SIMPLE_METHOD' HEADGOAL o tac o local_simpset_of);
+ (Method.SIMPLE_METHOD' o tac o local_simpset_of);
val perm_eq_meth = simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
val perm_eq_meth_debug = simp_meth_setup (perm_simp_tac DEBUG_tac);