src/HOLCF/Tools/domain/domain_extender.ML

 (* ----- calls for building new thy and thms -------------------------------- *)
 
 fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
   let
     val dtnvs = map ((fn (dname,vs) => 
-			 (Sign.full_name thy''' dname, map (Sign.read_typ thy''') vs))
+			 (Sign.full_name 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);
     fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
     val thy'' = thy''' |> Theory.add_types     (map thy_type  dtnvs)

     |> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
     |> Theory.parent_path
   end;
 
 val add_domain_i = gen_add_domain Sign.certify_typ;
-val add_domain = gen_add_domain Sign.read_typ;
+val add_domain = gen_add_domain Syntax.read_typ_global;
 
 
 (** outer syntax **)
 
 local structure P = OuterParse and K = OuterKeyword in