src/HOLCF/Fixrec.thy
changeset 35469 6e59de61d501
parent 35115 446c5063e4fd
child 35527 f4282471461d
     1.1 --- a/src/HOLCF/Fixrec.thy	Sun Feb 28 08:55:01 2010 -0800
     1.2 +++ b/src/HOLCF/Fixrec.thy	Sun Feb 28 09:22:53 2010 -0800
     1.3 @@ -265,7 +265,7 @@
     1.4  *}
     1.5  
     1.6  translations
     1.7 -  "x" <= "_match Fixrec.return (_variable x)"
     1.8 +  "x" <= "_match (CONST Fixrec.return) (_variable x)"
     1.9  
    1.10  
    1.11  subsection {* Pattern combinators for data constructors *}