src/HOLCF/ex/Domain_Proofs.thy

--- a/src/HOLCF/ex/Domain_Proofs.thy	Sat Nov 27 12:55:12 2010 -0800
+++ b/src/HOLCF/ex/Domain_Proofs.thy	Sat Nov 27 13:12:10 2010 -0800
@@ -467,7 +467,7 @@
 lemma lub_take_lemma:
   "(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
     = (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
-apply (simp only: thelub_Pair [symmetric] ch2ch_Pair chain_take_thms)
+apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
 apply (simp only: map_apply_thms pair_collapse)
 apply (simp only: fix_def2)
 apply (rule lub_eq)