1.1 --- a/src/HOLCF/Fixrec.thy	Mon Apr 13 09:29:55 2009 -0700
     1.2 +++ b/src/HOLCF/Fixrec.thy	Mon Apr 20 15:23:27 2009 -0700
     1.3 @@ -534,13 +534,13 @@
     1.4  
     1.5  lemma match_sinl_simps [simp]:
     1.6    "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x)\<cdot>k = k\<cdot>x"
     1.7 -  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x)\<cdot>k = fail"
     1.8 +  "y \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>y)\<cdot>k = fail"
     1.9    "match_sinl\<cdot>\<bottom>\<cdot>k = \<bottom>"
    1.10  by (simp_all add: match_sinl_def)
    1.11  
    1.12  lemma match_sinr_simps [simp]:
    1.13 -  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x)\<cdot>k = k\<cdot>x"
    1.14    "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x)\<cdot>k = fail"
    1.15 +  "y \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>y)\<cdot>k = k\<cdot>y"
    1.16    "match_sinr\<cdot>\<bottom>\<cdot>k = \<bottom>"
    1.17  by (simp_all add: match_sinr_def)
    1.18