src/HOLCF/Tools/domain/domain_syntax.ML
changeset 30364 577edc39b501
parent 30341 78d08e2d01b9
child 30912 4022298c1a86
     1.1 --- a/src/HOLCF/Tools/domain/domain_syntax.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4  in
     1.5    val dtype  = Type(dname,typevars);
     1.6    val dtype2 = foldr1 mk_ssumT (map prod cons');
     1.7 -  val dnam = NameSpace.base_name dname;
     1.8 +  val dnam = Long_Name.base_name dname;
     1.9    val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
    1.10    val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
    1.11    val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);