diff -r 3628064c4b44 -r 7be079726009 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Fri Jun 20 17:56:00 2008 +0200
+++ b/src/HOLCF/Porder.thy	Fri Jun 20 17:58:16 2008 +0200
@@ -326,7 +326,7 @@
 
 lemma bin_chainmax:
   "x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)"
-by (unfold max_in_chain_def, simp)
+unfolding max_in_chain_def by simp
 
 lemma lub_bin_chain:
   "x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y"