# HG changeset patch
# User huffman
# Date 1131224205 -3600
# Node ID 404f298220afe08e628f13d1624da69852052cfd
# Parent  587692219f69d47a31aa085dd127da0762a9eff8
simplify definitions

diff -r 587692219f69 -r 404f298220af src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Sat Nov 05 21:52:13 2005 +0100
+++ b/src/HOLCF/Fixrec.thy	Sat Nov 05 21:56:45 2005 +0100
@@ -143,13 +143,13 @@
   "match_up \<equiv> fup\<cdot>return"
 
   match_ONE :: "one \<rightarrow> unit maybe"
-  "match_ONE \<equiv> flift1 (\<lambda>u. return\<cdot>())"
-
+  "match_ONE \<equiv> \<Lambda> ONE. return\<cdot>()"
+ 
   match_TT :: "tr \<rightarrow> unit maybe"
-  "match_TT \<equiv> flift1 (\<lambda>b. if b then return\<cdot>() else fail)"
-
+  "match_TT \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi"
+ 
   match_FF :: "tr \<rightarrow> unit maybe"
-  "match_FF \<equiv> flift1 (\<lambda>b. if b then fail else return\<cdot>())"
+  "match_FF \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi"
 
 lemma match_UU_simps [simp]:
   "match_UU\<cdot>x = fail"
@@ -184,19 +184,19 @@
 lemma match_ONE_simps [simp]:
   "match_ONE\<cdot>ONE = return\<cdot>()"
   "match_ONE\<cdot>\<bottom> = \<bottom>"
-by (simp_all add: ONE_def match_ONE_def)
+by (simp_all add: match_ONE_def)
 
 lemma match_TT_simps [simp]:
   "match_TT\<cdot>TT = return\<cdot>()"
   "match_TT\<cdot>FF = fail"
   "match_TT\<cdot>\<bottom> = \<bottom>"
-by (simp_all add: TT_def FF_def match_TT_def)
+by (simp_all add: match_TT_def)
 
 lemma match_FF_simps [simp]:
   "match_FF\<cdot>FF = return\<cdot>()"
   "match_FF\<cdot>TT = fail"
   "match_FF\<cdot>\<bottom> = \<bottom>"
-by (simp_all add: TT_def FF_def match_FF_def)
+by (simp_all add: match_FF_def)
 
 subsection {* Mutual recursion *}