diff -r f2d75fd23124 -r e36a92ff543e src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed May 07 10:56:34 2008 +0200
+++ b/src/HOL/Inductive.thy	Wed May 07 10:56:35 2008 +0200
@@ -112,8 +112,8 @@
   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 unfolding Sup_set_def [symmetric]
-  by (rule lfp_ordinal_induct) 
+  using assms unfolding Sup_set_eq [symmetric]
+  by (rule lfp_ordinal_induct [where P=P])
 
 
 text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 
@@ -215,7 +215,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, assumption)
+apply (rule monoD [where f=f], assumption)
 apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
 done