--- a/src/HOL/Inductive.thy Wed Dec 28 15:08:12 2011 +0100
+++ b/src/HOL/Inductive.thy Wed Dec 28 20:03:13 2011 +0100
@@ -108,7 +108,7 @@
and P_f: "!!S. P S ==> P(f S)"
and P_Union: "!!M. !S:M. P S ==> P(Union M)"
shows "P(lfp f)"
- using assms by (rule lfp_ordinal_induct [where P=P])
+ using assms by (rule lfp_ordinal_induct)
text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct},
@@ -210,7 +210,7 @@
apply (rule Un_least [THEN Un_least])
apply (rule subset_refl, assumption)
apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
-apply (rule monoD [where f=f], assumption)
+apply (rule monoD, assumption)
apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
done