--- a/src/HOL/Lfp.thy Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Lfp.thy Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
The Knaster-Tarski Theorem
*)
-theory Lfp = Product_Type:
+theory Lfp
+import Product_Type
+begin
constdefs
lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"