# HG changeset patch
# User wenzelm
# Date 970685852 -7200
# Node ID 631628d6dd031d80ecc6a40da60178656e3271a0
# Parent  a068c666c53ef06c39b20ef48bf189913b57ca9d
'THEN', 'COMP': improved optional position arg;

diff -r a068c666c53e -r 631628d6dd03 src/Pure/Isar/attrib.ML
--- 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;