# HG changeset patch
# User huffman
# Date 1290958172 28800
# Node ID c52cd8bc426defc394569c625d1864f6b5d9c42d
# Parent  d28d41ee4cef2b6974a8ccd7957d1dc3800313ef
change match_bottom_simps to produce if-then-else, making more uses of bottom-patterns work with fixrec

diff -r d28d41ee4cef -r c52cd8bc426d src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Sat Nov 27 22:48:08 2010 -0800
+++ b/src/HOL/HOLCF/Fixrec.thy	Sun Nov 28 07:29:32 2010 -0800
@@ -150,9 +150,8 @@
   "match_FF = (\<Lambda> x k. If x then fail else k)"
 
 lemma match_bottom_simps [simp]:
-  "match_bottom\<cdot>\<bottom>\<cdot>k = \<bottom>"
-  "x \<noteq> \<bottom> \<Longrightarrow> match_bottom\<cdot>x\<cdot>k = fail"
-by (simp_all add: match_bottom_def)
+  "match_bottom\<cdot>x\<cdot>k = (if x = \<bottom> then \<bottom> else fail)"
+by (simp add: match_bottom_def)
 
 lemma match_Pair_simps [simp]:
   "match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"