COMP: optional position;

--- a/src/Pure/Isar/attrib.ML	Fri Jul 09 16:55:20 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Jul 09 18:44:58 1999 +0200
@@ -167,9 +167,9 @@
 
 (* COMP *)
 
-fun comp B (x, A) = (x, A COMP B);
+fun comp (i, B) (x, A) = (x, Drule.compose_single (A, i, B));
 
-fun gen_COMP thm = syntax (thm >> comp);
+fun gen_COMP thm = syntax (Scan.lift (Scan.optional Args.nat 1) -- thm >> comp);
 val global_COMP = gen_COMP global_thm;
 val local_COMP = gen_COMP local_thm;