diff -r f974a1c64348 -r 3dc4acca4388 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy	Fri Jan 18 20:22:07 2008 +0100
@@ -340,7 +340,7 @@
   shows "P x"
  apply (subgoal_tac "P (\<Squnion>i. basis_fun (\<lambda>a. principal (take i a))\<cdot>x)")
  apply (simp add: lub_basis_fun_take)
- apply (rule admD [rule_format, OF adm])
+ apply (rule admD [OF adm])
   apply (simp add: chain_basis_fun_take)
  apply (cut_tac x=x and i=i in basis_fun_take_eq_principal)
  apply (clarify, simp add: P)
@@ -452,7 +452,7 @@
 
 lemma compacts_lessD: "compacts x \<subseteq> compacts y \<Longrightarrow> x \<sqsubseteq> y"
 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
-apply (rule admD [rule_format], simp, simp)
+apply (rule admD, simp, simp)
 apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
 apply (simp add: compacts_def Abs_compact_basis_inverse approx_less)
 apply (simp add: compacts_def Abs_compact_basis_inverse)