--- a/src/HOL/Tools/recdef.ML Wed Aug 27 12:32:42 2014 +0200
+++ b/src/HOL/Tools/recdef.ML Wed Aug 27 14:54:32 2014 +0200
@@ -143,15 +143,15 @@
val recdef_wfN = "recdef_wf";
val recdef_modifiers =
- [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add): Method.modifier),
- Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add),
- Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del),
- Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add),
- Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add),
- Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del),
- Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add),
- Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add),
- Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del)] @
+ [Args.$$$ recdef_simpN -- Args.colon >> K (Method.modifier simp_add @{here}),
+ Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
+ Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
+ Args.$$$ recdef_congN -- Args.colon >> K (Method.modifier cong_add @{here}),
+ Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (Method.modifier cong_add @{here}),
+ Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (Method.modifier cong_del @{here}),
+ Args.$$$ recdef_wfN -- Args.colon >> K (Method.modifier wf_add @{here}),
+ Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (Method.modifier wf_add @{here}),
+ Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (Method.modifier wf_del @{here})] @
Clasimp.clasimp_modifiers;