fix too-specific types in lemmas match_{sinl,sinr}_simps
authorhuffman
Mon, 20 Apr 2009 15:23:27 -0700
changeset 30914 ceeb5f2eac75
parent 30913 10b26965a08f
child 30915 f8877f60e1ee
fix too-specific types in lemmas match_{sinl,sinr}_simps
src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Mon Apr 13 09:29:55 2009 -0700
+++ b/src/HOLCF/Fixrec.thy	Mon Apr 20 15:23:27 2009 -0700
@@ -534,13 +534,13 @@
 
 lemma match_sinl_simps [simp]:
   "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x)\<cdot>k = k\<cdot>x"
-  "x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x)\<cdot>k = fail"
+  "y \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>y)\<cdot>k = fail"
   "match_sinl\<cdot>\<bottom>\<cdot>k = \<bottom>"
 by (simp_all add: match_sinl_def)
 
 lemma match_sinr_simps [simp]:
-  "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x)\<cdot>k = k\<cdot>x"
   "x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x)\<cdot>k = fail"
+  "y \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>y)\<cdot>k = k\<cdot>y"
   "match_sinr\<cdot>\<bottom>\<cdot>k = \<bottom>"
 by (simp_all add: match_sinr_def)