diff -r 9f3826352b52 -r aa6296d09e0e src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Aug 27 12:32:42 2014 +0200
+++ b/src/Pure/simplifier.ML	Wed Aug 27 14:54:32 2014 +0200
@@ -332,21 +332,23 @@
 (** method syntax **)
 
 val cong_modifiers =
- [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
-  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
-  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del)];
+ [Args.$$$ congN -- Args.colon >> K (Method.modifier cong_add @{here}),
+  Args.$$$ congN -- Args.add -- Args.colon >> K (Method.modifier cong_add @{here}),
+  Args.$$$ congN -- Args.del -- Args.colon >> K (Method.modifier cong_del @{here})];
 
 val simp_modifiers =
- [Args.$$$ simpN -- Args.colon >> K (I, simp_add),
-  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
-  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
-  Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> K (Raw_Simplifier.clear_simpset, simp_add)]
+ [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add @{here}),
+  Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
+  Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
+  Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
+    K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = @{here}}]
    @ cong_modifiers;
 
 val simp_modifiers' =
- [Args.add -- Args.colon >> K (I, simp_add),
-  Args.del -- Args.colon >> K (I, simp_del),
-  Args.$$$ onlyN -- Args.colon >> K (Raw_Simplifier.clear_simpset, simp_add)]
+ [Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
+  Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
+  Args.$$$ onlyN -- Args.colon >>
+    K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = @{here}}]
    @ cong_modifiers;
 
 val simp_options =