author | huffman |
Sun, 28 Feb 2010 09:22:53 -0800 | |
changeset 35469 | 6e59de61d501 |
parent 35468 | 09bc6a2e2296 |
child 35470 | 13f3675c9644 |
--- a/src/HOLCF/Fixrec.thy Sun Feb 28 08:55:01 2010 -0800 +++ b/src/HOLCF/Fixrec.thy Sun Feb 28 09:22:53 2010 -0800 @@ -265,7 +265,7 @@ *} translations - "x" <= "_match Fixrec.return (_variable x)" + "x" <= "_match (CONST Fixrec.return) (_variable x)" subsection {* Pattern combinators for data constructors *}