src/HOLCF/Cfun.thy

--- a/src/HOLCF/Cfun.thy	Wed Jan 16 22:41:49 2008 +0100
+++ b/src/HOLCF/Cfun.thy	Thu Jan 17 00:51:20 2008 +0100
@@ -404,7 +404,7 @@
     \<Longrightarrow> \<forall>Y::nat \<Rightarrow> 'b. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
 apply clarify
 apply (drule_tac f=g in chain_monofun)
-apply (drule chfin [rule_format])
+apply (drule chfin)
 apply (unfold max_in_chain_def)
 apply (simp add: injection_eq)
 done