src/HOLCF/Cont.thy

--- a/src/HOLCF/Cont.thy	Tue Jan 15 16:19:23 2008 +0100
+++ b/src/HOLCF/Cont.thy	Wed Jan 16 22:41:49 2008 +0100
@@ -222,7 +222,7 @@
 
 lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun (f::'a::flat \<Rightarrow> 'b::pcpo)"
 apply (rule monofunI)
-apply (drule ax_flat [rule_format])
+apply (drule ax_flat)
 apply auto
 done