hide common name of constant 'run'
authorhuffman
Thu Apr 13 23:14:18 2006 +0200 (2006-04-13)
changeset 1943927c2e4cd634b
parent 19438 6d266e266b3f
child 19440 b2877e230b07
hide common name of constant 'run'
src/HOLCF/Fixrec.thy
     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