Args.addN, Args.delN;

--- a/src/Provers/clasimp.ML	Wed Sep 13 22:29:37 2000 +0200
+++ b/src/Provers/clasimp.ML	Wed Sep 13 22:31:19 2000 +0200
@@ -272,13 +272,11 @@
 (* method modifiers *)
 
 val iffN = "iff";
-val addN = "add";
-val delN = "del";
 
 val iff_modifiers =
  [Args.$$$ iffN -- Args.colon >> K ((I, iff_add_local): Method.modifier),
-  Args.$$$ iffN -- Args.$$$ addN -- Args.colon >> K (I, iff_add_local),
-  Args.$$$ iffN -- Args.$$$ delN -- Args.colon >> K (I, iff_del_local)];
+  Args.$$$ iffN -- Args.$$$ Args.addN -- Args.colon >> K (I, iff_add_local),
+  Args.$$$ iffN -- Args.$$$ Args.delN -- Args.colon >> K (I, iff_del_local)];
 
 val clasimp_modifiers =
   Simplifier.simp_modifiers @ Splitter.split_modifiers @

--- a/src/Provers/classical.ML	Wed Sep 13 22:29:37 2000 +0200
+++ b/src/Provers/classical.ML	Wed Sep 13 22:31:19 2000 +0200
@@ -1027,7 +1027,6 @@
 val elimN = "elim";
 val destN = "dest";
 val ruleN = "rule";
-val delN = "del";
 
 val colon = Args.$$$ ":";
 val query = Args.$$$ "?";
@@ -1040,7 +1039,7 @@
 
 fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h);
 
-fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ delN) >> K att);
+fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ Args.delN) >> K att);
 val rule_del_attr = (del_args rule_del_global, del_args rule_del_local);
 
 
@@ -1159,7 +1158,7 @@
   Args.$$$ introN -- query_colon >> K (I, xtra_intro_local),
   Args.$$$ introN -- bang_colon >> K (I, safe_intro_local),
   Args.$$$ introN -- colon >> K (I, haz_intro_local),
-  Args.$$$ delN -- colon >> K (I, rule_del_local)];
+  Args.$$$ Args.delN -- colon >> K (I, rule_del_local)];
 
 fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));

--- a/src/Provers/simplifier.ML	Wed Sep 13 22:29:37 2000 +0200
+++ b/src/Provers/simplifier.ML	Wed Sep 13 22:31:19 2000 +0200
@@ -460,8 +460,6 @@
 
 val simpN = "simp";
 val congN = "cong";
-val addN = "add";
-val delN = "del";
 val onlyN = "only";
 val no_asmN = "no_asm";
 val no_asm_useN = "no_asm_use";
@@ -518,19 +516,19 @@
 
 val cong_modifiers =
  [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier),
-  Args.$$$ congN -- Args.$$$ addN -- Args.colon >> K (I, cong_add_local),
-  Args.$$$ congN -- Args.$$$ delN -- Args.colon >> K (I, cong_del_local)];
+  Args.$$$ congN -- Args.$$$ Args.addN -- Args.colon >> K (I, cong_add_local),
+  Args.$$$ congN -- Args.$$$ Args.delN -- Args.colon >> K (I, cong_del_local)];
 
 val simp_modifiers =
  [Args.$$$ simpN -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ simpN -- Args.$$$ addN -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ simpN -- Args.$$$ delN -- Args.colon >> K (I, simp_del_local),
+  Args.$$$ simpN -- Args.$$$ Args.addN -- Args.colon >> K (I, simp_add_local),
+  Args.$$$ simpN -- Args.$$$ Args.delN -- Args.colon >> K (I, simp_del_local),
   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
    @ cong_modifiers;
 
 val simp_modifiers' =
- [Args.$$$ addN -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ delN -- Args.colon >> K (I, simp_del_local),
+ [Args.$$$ Args.addN -- Args.colon >> K (I, simp_add_local),
+  Args.$$$ Args.delN -- Args.colon >> K (I, simp_del_local),
   Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
    @ cong_modifiers;
 

--- a/src/Provers/splitter.ML	Wed Sep 13 22:29:37 2000 +0200
+++ b/src/Provers/splitter.ML	Wed Sep 13 22:31:19 2000 +0200
@@ -417,8 +417,8 @@
 
 val split_modifiers =
  [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier),
-  Args.$$$ splitN -- Args.$$$ "add" -- Args.colon >> K (I, split_add_local),
-  Args.$$$ splitN -- Args.$$$ "del" -- Args.colon >> K (I, split_del_local)];
+  Args.$$$ splitN -- Args.$$$ Args.addN -- Args.colon >> K (I, split_add_local),
+  Args.$$$ splitN -- Args.$$$ Args.delN -- Args.colon >> K (I, split_del_local)];
 
 val split_args = #2 oo Method.syntax (Args.mode "asm" -- Attrib.local_thms);
 

--- a/src/Pure/Isar/args.ML	Wed Sep 13 22:29:37 2000 +0200
+++ b/src/Pure/Isar/args.ML	Wed Sep 13 22:31:19 2000 +0200
@@ -29,6 +29,8 @@
   val nat: T list -> int * T list
   val int: T list -> int * T list
   val var: T list -> indexname * T list
+  val addN: string
+  val delN: string
   val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
@@ -135,6 +137,9 @@
 val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
 val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
 
+val addN = "add";
+val delN = "del";
+
 
 (* enumerations *)
 

--- a/src/Pure/Isar/attrib.ML	Wed Sep 13 22:29:37 2000 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Sep 13 22:31:19 2000 +0200
@@ -156,8 +156,8 @@
 
 fun no_args x = syntax (Scan.succeed x);
 
-fun add_del_args add del x =
-  syntax (Scan.lift (Args.$$$ "add" >> K add || Args.$$$ "del" >> K del || Scan.succeed add)) x;
+fun add_del_args add del x = syntax (Scan.lift
+    (Args.$$$ Args.addN >> K add || Args.$$$ Args.delN >> K del || Scan.succeed add)) x;
 
 
 

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