| changeset 35469 | 6e59de61d501 |
| parent 35115 | 446c5063e4fd |
| child 35527 | f4282471461d |
--- 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 *}