--- 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