--- a/src/HOLCF/LowerPD.thy Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/LowerPD.thy Fri Jan 18 20:22:07 2008 +0100
@@ -376,7 +376,7 @@
apply (rule iffI)
apply (subgoal_tac
"adm (\<lambda>f. f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
- apply (drule admD [rule_format], rule chain_approx)
+ apply (drule admD, rule chain_approx)
apply (drule_tac f="approx i" in monofun_cfun_arg)
apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_lower_principal, simp)