'THEN', 'COMP': improved optional position arg;

--- a/src/Pure/Isar/attrib.ML	Wed Oct 04 20:55:57 2000 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Oct 04 20:57:32 2000 +0200
@@ -173,7 +173,7 @@
 
 fun comp (i, B) (x, A) = (x, Drule.compose_single (A, i, B));
 
-fun gen_COMP thm = syntax (Scan.lift (Scan.optional Args.nat 1) -- thm >> comp);
+fun gen_COMP thm = syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm >> comp);
 val COMP_global = gen_COMP global_thm;
 val COMP_local = gen_COMP local_thm;
 
@@ -182,7 +182,7 @@
 
 fun resolve (i, B) (x, A) = (x, A RSN (i, B));
 
-fun gen_RS thm = syntax (Scan.lift (Scan.optional Args.nat 1) -- thm >> resolve);
+fun gen_RS thm = syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm >> resolve);
 val RS_global = gen_RS global_thm;
 val RS_local = gen_RS local_thm;