1.1 --- a/src/HOL/Library/Executable_Set.thy	Tue Oct 06 15:59:12 2009 +0200
     1.2 +++ b/src/HOL/Library/Executable_Set.thy	Tue Oct 06 18:27:00 2009 +0200
     1.3 @@ -74,11 +74,12 @@
     1.4  types_code
     1.5    fset ("(_/ \<module>fset)")
     1.6  attach {*
     1.7 -datatype 'a fset = Set of 'a list;
     1.8 +datatype 'a fset = Set of 'a list | Coset of 'a list;
     1.9  *}
    1.10  
    1.11  consts_code
    1.12    Set ("\<module>Set")
    1.13 +  Coset ("\<module>Coset")
    1.14  
    1.15  consts_code
    1.16    "empty"             ("{*Fset.empty*}")