| changeset 9952 | 24914e42b857 |
| parent 9938 | cb6a7572d0a1 |
| child 10008 | 61eb9f3aa92a |
--- a/src/Pure/Isar/method.ML Wed Sep 13 22:29:37 2000 +0200 +++ b/src/Pure/Isar/method.ML Wed Sep 13 22:31:19 2000 +0200 @@ -199,7 +199,7 @@ val intro_local = mk_att LocalRules.map add_intro; val rule_del_local = mk_att LocalRules.map del_rule; -fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ "del") >> K att); +fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ Args.delN) >> K att); end;