--- a/src/HOL/Fun.thy Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Fun.thy Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
Notions about functions.
*)
-theory Fun = Typedef:
+theory Fun
+import Typedef
+begin
instance set :: (type) order
by (intro_classes,