--- a/src/HOLCF/Fixrec.thy Thu Apr 13 12:01:16 2006 +0200
+++ b/src/HOLCF/Fixrec.thy Thu Apr 13 23:14:18 2006 +0200
@@ -191,7 +191,7 @@
"_Case1" :: "['a, 'b] => Case_syn" ("(2_ \<Rightarrow>/ _)" 10)
translations
- "_Case_syntax x ms" == "run\<cdot>(ms\<cdot>x)"
+ "_Case_syntax x ms" == "Fixrec.run\<cdot>(ms\<cdot>x)"
"_Case2 m ms" == "m \<parallel> ms"
text {* Parsing Case expressions *}
@@ -544,6 +544,6 @@
use "fixrec_package.ML"
-hide (open) const return bind fail
+hide (open) const return bind fail run
end