src/HOL/Product_Type.thy

--- a/src/HOL/Product_Type.thy	Wed Apr 15 15:30:37 2009 +0200
+++ b/src/HOL/Product_Type.thy	Wed Apr 15 15:30:38 2009 +0200
@@ -84,6 +84,14 @@
 lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
   by (rule ext) simp
 
+instantiation unit :: default
+begin
+
+definition "default = ()"
+
+instance ..
+
+end
 
 text {* code generator setup *}