src/HOL/Inductive.thy

--- a/src/HOL/Inductive.thy	Wed Sep 16 09:04:41 2009 +0200
+++ b/src/HOL/Inductive.thy	Wed Sep 16 13:43:05 2009 +0200
@@ -111,8 +111,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 unfolding Sup_set_eq [symmetric]
-  by (rule lfp_ordinal_induct [where P=P])
+  using assms by (rule lfp_ordinal_induct [where P=P])
 
 
 text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct},