# 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;