src/HOLCF/Tools/domain/domain_extender.ML
changeset 28965 1de908189869
parent 28536 8dccb6035d0f
child 29585 c23295521af5
--- a/src/HOLCF/Tools/domain/domain_extender.ML	Wed Dec 03 21:00:39 2008 -0800
+++ b/src/HOLCF/Tools/domain/domain_extender.ML	Thu Dec 04 14:43:33 2008 +0100
@@ -100,7 +100,7 @@
 fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
   let
     val dtnvs = map ((fn (dname,vs) => 
-			 (Sign.full_name thy''' dname, map (Syntax.read_typ_global thy''') vs))
+			 (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
                    o fst) eqs''';
     val cons''' = map snd eqs''';
     fun thy_type  (dname,tvars)  = (Sign.base_name dname, length tvars, NoSyn);