src/HOLCF/Fixrec.thy
changeset 19104 7d69b6d7b8f1
parent 19092 e32cf29f01fc
child 19327 4565e230e6eb
     1.1 --- a/src/HOLCF/Fixrec.thy	Sat Feb 18 18:08:23 2006 +0100
     1.2 +++ b/src/HOLCF/Fixrec.thy	Sun Feb 19 01:40:13 2006 +0100
     1.3 @@ -208,7 +208,7 @@
     1.4  parse_translation {*
     1.5  (* rewrites (_pat x) => (return) *)
     1.6  (* rewrites (_var x t) => (Abs_CFun (%x. t)) *)
     1.7 -  [("_pat", K (Syntax.const "return")),
     1.8 +  [("_pat", K (Syntax.const "Fixrec.return")),
     1.9     mk_binder_tr ("_var", "Abs_CFun")];
    1.10  *}
    1.11  
    1.12 @@ -242,7 +242,7 @@
    1.13  *}
    1.14  
    1.15  translations
    1.16 -  "x" <= "_match return (_var x)"
    1.17 +  "x" <= "_match Fixrec.return (_var x)"
    1.18  
    1.19  
    1.20  subsection {* Pattern combinators for data constructors *}
    1.21 @@ -540,4 +540,9 @@
    1.22  
    1.23  use "fixrec_package.ML"
    1.24  
    1.25 +setup {*
    1.26 +  Theory.hide_consts_i false
    1.27 +    ["Fixrec.return", "Fixrec.bind", "Fixrec.fail"]
    1.28 +*}
    1.29 +
    1.30  end