1.1 --- a/src/HOL/Product_Type.thy	Wed Apr 15 15:30:37 2009 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Apr 15 15:30:38 2009 +0200
     1.3 @@ -84,6 +84,14 @@
     1.4  lemma unit_abs_eta_conv [simp,noatp]: "(%u::unit. f ()) = f"
     1.5    by (rule ext) simp
     1.6  
     1.7 +instantiation unit :: default
     1.8 +begin
     1.9 +
    1.10 +definition "default = ()"
    1.11 +
    1.12 +instance ..
    1.13 +
    1.14 +end
    1.15  
    1.16  text {* code generator setup *}
    1.17