# HG changeset patch
# User huffman
# Date 1140309613 -3600
# Node ID 7d69b6d7b8f196e37b59fa7b81bd39038b76b1c0
# Parent  0eb600479944e3847ba608b57d04979395914c33
use qualified name for return

diff -r 0eb600479944 -r 7d69b6d7b8f1 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Sat Feb 18 18:08:23 2006 +0100
+++ b/src/HOLCF/Fixrec.thy	Sun Feb 19 01:40:13 2006 +0100
@@ -208,7 +208,7 @@
 parse_translation {*
 (* rewrites (_pat x) => (return) *)
 (* rewrites (_var x t) => (Abs_CFun (%x. t)) *)
-  [("_pat", K (Syntax.const "return")),
+  [("_pat", K (Syntax.const "Fixrec.return")),
    mk_binder_tr ("_var", "Abs_CFun")];
 *}
 
@@ -242,7 +242,7 @@
 *}
 
 translations
-  "x" <= "_match return (_var x)"
+  "x" <= "_match Fixrec.return (_var x)"
 
 
 subsection {* Pattern combinators for data constructors *}
@@ -540,4 +540,9 @@
 
 use "fixrec_package.ML"
 
+setup {*
+  Theory.hide_consts_i false
+    ["Fixrec.return", "Fixrec.bind", "Fixrec.fail"]
+*}
+
 end