use Args.colon / Args.parens;

--- a/src/HOL/Tools/induct_method.ML	Fri May 05 22:30:14 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML	Fri May 05 22:32:25 2000 +0200
@@ -364,7 +364,7 @@
 
 (* attributes *)
 
-fun spec k = (Args.$$$ k -- Args.$$$ ":") |-- Args.!!! Args.name;
+fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name;
 
 fun attrib sign_of add_type add_set = Scan.depend (fn x =>
   let val sg = sign_of x in
@@ -395,18 +395,18 @@
       spec typeN >> (err typeN (get_type ctxt) o Sign.intern_tycon sg) ||
       spec setN >> (err setN (get_set ctxt) o Sign.intern_const sg)
     end >> pair ctxt) ||
-  Scan.lift (Args.$$$ ruleN -- Args.$$$ ":") |-- Attrib.local_thm;
+  Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.local_thm;
 
 val cases_rule = rule lookup_casesT lookup_casesS;
 val induct_rule = rule lookup_inductT lookup_inductS;
 
-val kind = (Args.$$$ typeN || Args.$$$ setN || Args.$$$ ruleN) -- Args.$$$ ":";
+val kind = (Args.$$$ typeN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon;
 val term = Scan.unless (Scan.lift kind) Args.local_term;
 val term_dummy = Scan.unless (Scan.lift kind)
   (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
 
 fun mode name =
-  Scan.lift (Scan.optional (Args.$$$ name -- Args.$$$ ":" >> K true) false);
+  Scan.lift (Scan.optional (Args.parens (Args.$$$ name) >> K true) false);
 
 in
 

--- a/src/Provers/simplifier.ML	Fri May 05 22:30:14 2000 +0200
+++ b/src/Provers/simplifier.ML	Fri May 05 22:32:25 2000 +0200
@@ -479,26 +479,24 @@
 
 (* simplification *)
 
-val colon = Args.$$$ ":";
-
 val simp_options =
- (Args.$$$ "no_asm" -- colon >> K simp_tac ||
-  Args.$$$ "no_asm_simp" -- colon >> K asm_simp_tac ||
-  Args.$$$ "no_asm_use" -- colon >> K full_simp_tac ||
+ (Args.parens (Args.$$$ "no_asm") >> K simp_tac ||
+  Args.parens (Args.$$$ "no_asm_simp") >> K asm_simp_tac ||
+  Args.parens (Args.$$$ "no_asm_use") >> K full_simp_tac ||
   Scan.succeed asm_full_simp_tac);
 
 val simp_modifiers =
- [Args.$$$ simpN -- colon >> K (I, simp_add_local),
-  Args.$$$ simpN -- Args.$$$ addN -- colon >> K (I, simp_add_local),
-  Args.$$$ simpN -- Args.$$$ delN -- colon >> K (I, simp_del_local),
-  Args.$$$ simpN -- Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local),
-  Args.$$$ otherN -- colon >> K (I, I)];
+ [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.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local),
+  Args.$$$ otherN -- Args.colon >> K (I, I)];
 
 val simp_modifiers' =
- [Args.$$$ addN -- colon >> K (I, simp_add_local),
-  Args.$$$ delN -- colon >> K (I, simp_del_local),
-  Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local),
-  Args.$$$ otherN -- colon >> K (I, I)];
+ [Args.$$$ addN -- Args.colon >> K (I, simp_add_local),
+  Args.$$$ delN -- Args.colon >> K (I, simp_del_local),
+  Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local),
+  Args.$$$ otherN -- Args.colon >> K (I, I)];
 
 fun simp_args more_mods =
   Method.sectioned_args (Args.bang_facts -- Scan.lift simp_options) (more_mods @ simp_modifiers');

--- a/src/Provers/splitter.ML	Fri May 05 22:30:14 2000 +0200
+++ b/src/Provers/splitter.ML	Fri May 05 22:32:25 2000 +0200
@@ -415,9 +415,9 @@
 (* method modifiers *)
 
 val split_modifiers =
- [Args.$$$ splitN -- Args.$$$ ":" >> K ((I, split_add_local): Method.modifier),
-  Args.$$$ splitN -- Args.$$$ "add" -- Args.$$$ ":" >> K (I, split_add_local),
-  Args.$$$ splitN -- Args.$$$ "del" -- Args.$$$ ":" >> K (I, split_del_local)];
+ [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)];