1.1 --- a/src/HOLCF/Fixrec.thy	Sat Nov 27 12:26:18 2010 -0800
     1.2 +++ b/src/HOLCF/Fixrec.thy	Sat Nov 27 12:27:57 2010 -0800
     1.3 @@ -105,9 +105,9 @@
     1.4  default_sort pcpo
     1.5  
     1.6  definition
     1.7 -  match_UU :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
     1.8 +  match_bottom :: "'a \<rightarrow> 'c match \<rightarrow> 'c match"
     1.9  where
    1.10 -  "match_UU = (\<Lambda> x k. seq\<cdot>x\<cdot>fail)"
    1.11 +  "match_bottom = (\<Lambda> x k. seq\<cdot>x\<cdot>fail)"
    1.12  
    1.13  definition
    1.14    match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match"
    1.15 @@ -149,10 +149,10 @@
    1.16  where
    1.17    "match_FF = (\<Lambda> x k. If x then fail else k)"
    1.18  
    1.19 -lemma match_UU_simps [simp]:
    1.20 -  "match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>"
    1.21 -  "x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail"
    1.22 -by (simp_all add: match_UU_def)
    1.23 +lemma match_bottom_simps [simp]:
    1.24 +  "match_bottom\<cdot>\<bottom>\<cdot>k = \<bottom>"
    1.25 +  "x \<noteq> \<bottom> \<Longrightarrow> match_bottom\<cdot>x\<cdot>k = fail"
    1.26 +by (simp_all add: match_bottom_def)
    1.27  
    1.28  lemma match_Pair_simps [simp]:
    1.29    "match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y"
    1.30 @@ -244,7 +244,7 @@
    1.31        (@{const_name ONE}, @{const_name match_ONE}),
    1.32        (@{const_name TT}, @{const_name match_TT}),
    1.33        (@{const_name FF}, @{const_name match_FF}),
    1.34 -      (@{const_name UU}, @{const_name match_UU}) ]
    1.35 +      (@{const_name UU}, @{const_name match_bottom}) ]
    1.36  *}
    1.37  
    1.38  hide_const (open) succeed fail run