src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
changeset 41296 6aaf80ea9715
parent 40853 225698654b2a
child 41429 cf5f025bc3c7
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Dec 19 18:11:20 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Dec 19 18:15:21 2010 -0800
     1.3 @@ -34,7 +34,7 @@
     1.4  end
     1.5  
     1.6  
     1.7 -structure Domain_Constructors :> DOMAIN_CONSTRUCTORS =
     1.8 +structure Domain_Constructors : DOMAIN_CONSTRUCTORS =
     1.9  struct
    1.10  
    1.11  open HOLCF_Library