# HG changeset patch
# User huffman
# Date 1240266207 25200
# Node ID ceeb5f2eac757e99ad2dbdda901f54e0cbc104a9
# Parent  10b26965a08f984a1b0852784c78424e70214d28
fix too-specific types in lemmas match_{sinl,sinr}_simps

diff -r 10b26965a08f -r ceeb5f2eac75 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)