src/HOLCF/Fixrec.thy
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"