# HG changeset patch
# User wenzelm
# Date 954532527 -7200
# Node ID 3f34637cb9c0af76a7d255aa56a4f7a459849984
# Parent  427ead639d8ae6288c10f3ba83960144067d9a81
use Attrib.add_del_args;

diff -r 427ead639d8a -r 3f34637cb9c0 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Mar 31 21:54:50 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri Mar 31 21:55:27 2000 +0200
@@ -124,7 +124,8 @@
     else [thm]
   end;
 
-(* mono add/del *)
+
+(* attributes *)
 
 local
 
@@ -136,24 +137,13 @@
 fun mk_att f g (x, thm) = (f (g thm) x, thm);
 
 in
-
-val mono_add_global = mk_att map_rules_global add_mono;
-val mono_del_global = mk_att map_rules_global del_mono;
-
+  val mono_add_global = mk_att map_rules_global add_mono;
+  val mono_del_global = mk_att map_rules_global del_mono;
 end;
 
-
-(* concrete syntax *)
-
-val monoN = "mono";
-val addN = "add";
-val delN = "del";
-
-fun mono_att add del =
-  Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add));
-
 val mono_attr =
-  (mono_att mono_add_global mono_del_global, mono_att Attrib.undef_local_attribute Attrib.undef_local_attribute);
+ (Attrib.add_del_args mono_add_global mono_del_global,
+  Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
 
 
 
@@ -824,8 +814,9 @@
 
 (* setup theory *)
 
-val setup = [InductiveData.init,
-             Attrib.add_attributes [(monoN, mono_attr, "monotonicity rule")]];
+val setup =
+ [InductiveData.init,
+  Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]];
 
 
 (* outer syntax *)
diff -r 427ead639d8a -r 3f34637cb9c0 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Fri Mar 31 21:54:50 2000 +0200
+++ b/src/Provers/simplifier.ML	Fri Mar 31 21:55:27 2000 +0200
@@ -451,15 +451,9 @@
 val onlyN = "only";
 val otherN = "other";
 
-fun simp_att change =
-  (Args.$$$ addN >> K (op addsimps) ||
-    Args.$$$ delN >> K (op delsimps) ||
-    Scan.succeed (op addsimps))
-  >> change
-  |> Scan.lift
-  |> Attrib.syntax;
-
-val simp_attr = (simp_att change_global_ss, simp_att change_local_ss);
+val simp_attr =
+ (Attrib.add_del_args simp_add_global simp_del_global,
+  Attrib.add_del_args simp_add_local simp_del_local);
 
 
 (* conversions *)
diff -r 427ead639d8a -r 3f34637cb9c0 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Fri Mar 31 21:54:50 2000 +0200
+++ b/src/Provers/splitter.ML	Fri Mar 31 21:55:27 2000 +0200
@@ -398,33 +398,26 @@
 (* attributes *)
 
 val splitN = "split";
-val addN = "add";
-val delN = "del";
-
-fun split_att change =
-  (Args.$$$ addN >> K (op addsplits) ||
-    Args.$$$ delN >> K (op delsplits) ||
-    Scan.succeed (op addsplits))
-  >> change
-  |> Scan.lift
-  |> Attrib.syntax;
-
-val setup_attrs = Attrib.add_attributes
- [(splitN, (split_att Simplifier.change_global_ss, split_att Simplifier.change_local_ss),
-    "declare splitter rule")];
 
 val split_add_global = Simplifier.change_global_ss (op addsplits);
 val split_del_global = Simplifier.change_global_ss (op delsplits);
 val split_add_local = Simplifier.change_local_ss (op addsplits);
 val split_del_local = Simplifier.change_local_ss (op delsplits);
 
+val split_attr =
+ (Attrib.add_del_args split_add_global split_del_global,
+  Attrib.add_del_args split_add_local split_del_local);
+
+val setup_attrs =
+  Attrib.add_attributes [(splitN, split_attr, "declare splitter rule")];
+
 
 (* method modifiers *)
 
 val split_modifiers =
  [Args.$$$ splitN -- Args.$$$ ":" >> K ((I, split_add_local): Method.modifier),
-  Args.$$$ splitN -- Args.$$$ addN -- Args.$$$ ":" >> K (I, split_add_local),
-  Args.$$$ splitN -- Args.$$$ delN -- Args.$$$ ":" >> K (I, split_del_local)];
+  Args.$$$ splitN -- Args.$$$ "add" -- Args.$$$ ":" >> K (I, split_add_local),
+  Args.$$$ splitN -- Args.$$$ "del" -- Args.$$$ ":" >> K (I, split_del_local)];
 
 
 
diff -r 427ead639d8a -r 3f34637cb9c0 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Fri Mar 31 21:54:50 2000 +0200
+++ b/src/Pure/Isar/calculation.ML	Fri Mar 31 21:55:27 2000 +0200
@@ -91,15 +91,9 @@
 
 (* concrete syntax *)
 
-val transN = "trans";
-val addN = "add";
-val delN = "del";
-
-fun trans_att add del =
-  Attrib.syntax (Scan.lift (Args.$$$ addN >> K add || Args.$$$ delN >> K del || Scan.succeed add));
-
 val trans_attr =
-  (trans_att trans_add_global trans_del_global, trans_att trans_add_local trans_del_local);
+ (Attrib.add_del_args trans_add_global trans_del_global,
+  Attrib.add_del_args trans_add_local trans_del_local);
 
 
 
@@ -181,7 +175,7 @@
 (** theory setup **)
 
 val setup = [GlobalCalculation.init, LocalCalculation.init,
-  Attrib.add_attributes [(transN, trans_attr, "declare transitivity rule")]];
+  Attrib.add_attributes [("trans", trans_attr, "declare transitivity rule")]];
 
 
 end;