| changeset 17057 | 0934ac31985f |
| parent 16394 | 495dbcd4f4c9 |
| child 17325 | d9d50222808e |
--- a/src/HOLCF/domain/extender.ML Tue Aug 16 13:42:23 2005 +0200 +++ b/src/HOLCF/domain/extender.ML Tue Aug 16 13:42:26 2005 +0200 @@ -140,7 +140,7 @@ (** outer syntax **) -local structure P = OuterParse and K = OuterSyntax.Keyword in +local structure P = OuterParse and K = OuterKeyword in val dest_decl = P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --