diff -r 82e8b18e6985 -r 8b09c29453ac src/HOL/WF_Rel.thy
--- a/src/HOL/WF_Rel.thy	Sun Jul 16 20:53:19 2000 +0200
+++ b/src/HOL/WF_Rel.thy	Sun Jul 16 20:53:35 2000 +0200
@@ -13,7 +13,9 @@
 WF_Rel = Finite +
 
 (* actually belongs to Finite.thy *)
-instance "*" :: (finite,finite) finite   (finite_Prod) 
+instance unit :: finite                  (finite_unit)
+instance "*" :: (finite,finite) finite   (finite_Prod)
+
 
 consts
   less_than :: "(nat*nat)set"