src/HOLCF/domain/extender.ML

--- a/src/HOLCF/domain/extender.ML	Sat Apr 14 11:05:12 2007 +0200
+++ b/src/HOLCF/domain/extender.ML	Sat Apr 14 17:35:52 2007 +0200
@@ -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 (str2typ thy''') vs))
+			 (Sign.full_name thy''' dname, map (Sign.read_typ thy''') vs))
                    o fst) eqs''';
     val cons''' = map snd eqs''';
     fun thy_type  (dname,tvars)  = (Sign.base_name dname, length tvars, NoSyn);
@@ -139,7 +139,7 @@
   end;
 
 val add_domain_i = gen_add_domain Sign.certify_typ;
-val add_domain = gen_add_domain str2typ;
+val add_domain = gen_add_domain Sign.read_typ;
 
 
 (** outer syntax **)