src/HOLCF/Fixrec.thy
changeset 19439 27c2e4cd634b
parent 19396 0592ea0c68a0
child 23152 9497234a2743
     1.1 --- a/src/HOLCF/Fixrec.thy	Thu Apr 13 12:01:16 2006 +0200
     1.2 +++ b/src/HOLCF/Fixrec.thy	Thu Apr 13 23:14:18 2006 +0200
     1.3 @@ -191,7 +191,7 @@
     1.4    "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
     1.5  
     1.6  translations
     1.7 -  "_Case_syntax x ms" == "run\<cdot>(ms\<cdot>x)"
     1.8 +  "_Case_syntax x ms" == "Fixrec.run\<cdot>(ms\<cdot>x)"
     1.9    "_Case2 m ms" == "m \<parallel> ms"
    1.10  
    1.11  text {* Parsing Case expressions *}
    1.12 @@ -544,6 +544,6 @@
    1.13  
    1.14  use "fixrec_package.ML"
    1.15  
    1.16 -hide (open) const return bind fail
    1.17 +hide (open) const return bind fail run
    1.18  
    1.19  end