| changeset 6948 | 01f3c7866ead |
| parent 6933 | 0890fde41522 |
| child 7367 | a79d4683fadf |
--- 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;