# HG changeset patch
# User wenzelm
# Date 931538698 -7200
# Node ID 01f3c7866ead265aec44877321e3ad3d8e411a5d
# Parent  a233bc746c75e8f6d6f5f3e2d69ed9454057c8fa
COMP: optional position;

diff -r a233bc746c75 -r 01f3c7866ead src/Pure/Isar/attrib.ML
--- 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;