# HG changeset patch
# User huffman
# Date 1267377773 28800
# Node ID 6e59de61d501707ab133d4ca97dd5f6a9a5ba048
# Parent  09bc6a2e22966d220959fdae633b4c57b81b4ac2
fix output translation for Case syntax

diff -r 09bc6a2e2296 -r 6e59de61d501 src/HOLCF/Fixrec.thy
--- 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 *}