src/HOLCF/Tools/domain/domain_syntax.ML
changeset 30280 eb98b49ef835
parent 30190 479806475f3c
child 30341 78d08e2d01b9
--- a/src/HOLCF/Tools/domain/domain_syntax.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -25,7 +25,7 @@
 in
   val dtype  = Type(dname,typevars);
   val dtype2 = foldr1 mk_ssumT (map prod cons');
-  val dnam = Sign.base_name dname;
+  val dnam = NameSpace.base_name dname;
   val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
   val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
   val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);