# HG changeset patch
# User wenzelm
# Date 969400320 -7200
# Node ID 1823b34834fdafa3a3b7f7f6ccb89466f4ddb864
# Parent  12fd0fcf755af00fbbda60e2fbf5f2c1196da905
tuned;

diff -r 12fd0fcf755a -r 1823b34834fd src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Tue Sep 19 23:51:39 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Tue Sep 19 23:52:00 2000 +0200
@@ -188,14 +188,14 @@
 
 val recdef_modifiers =
  [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add_local): Method.modifier),
-  Args.$$$ recdef_simpN -- Args.$$$ Args.addN -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ recdef_simpN -- Args.$$$ Args.delN -- Args.colon >> K (I, simp_del_local),
+  Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
+  Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
   Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add_local),
-  Args.$$$ recdef_congN -- Args.$$$ Args.addN -- Args.colon >> K (I, cong_add_local),
-  Args.$$$ recdef_congN -- Args.$$$ Args.delN -- Args.colon >> K (I, cong_del_local),
+  Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add_local),
+  Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del_local),
   Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add_local),
-  Args.$$$ recdef_wfN -- Args.$$$ Args.addN -- Args.colon >> K (I, wf_add_local),
-  Args.$$$ recdef_wfN -- Args.$$$ Args.delN -- Args.colon >> K (I, wf_del_local)] @
+  Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add_local),
+  Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del_local)] @
   Clasimp.clasimp_modifiers;