changeset 40046 | ba2e41c8b725 |
parent 39807 | 19ddbededdd3 |
child 40322 | 707eb30e8a53 |
--- a/src/HOLCF/Fixrec.thy Wed Oct 20 17:25:22 2010 -0700 +++ b/src/HOLCF/Fixrec.thy Wed Oct 20 19:40:02 2010 -0700 @@ -115,7 +115,7 @@ definition match_UU :: "'a \<rightarrow> 'c match \<rightarrow> 'c match" where - "match_UU = strictify\<cdot>(\<Lambda> x k. fail)" + "match_UU = (\<Lambda> x k. strict\<cdot>x\<cdot>fail)" definition match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"