--- a/src/HOLCF/Fix.thy Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/Fix.thy Fri Jan 18 20:22:07 2008 +0100
@@ -153,7 +153,7 @@
lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
apply (subst fix_def2)
-apply (erule admD [rule_format])
+apply (erule admD)
apply (rule chain_iterate)
apply (induct_tac "i", simp_all)
done
@@ -233,7 +233,7 @@
apply (intro strip)
apply (erule admD)
apply (rule chain_iterate)
-apply assumption
+apply (erule spec)
done
text {* computational induction for weak admissible formulae *}