src/HOLCF/Tools/domain/domain_extender.ML

   let
     val dtnvs = map ((fn (dname,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)  = (NameSpace.base_name dname, length tvars, NoSyn);
+    fun thy_type  (dname,tvars)  = (Binding.name (NameSpace.base_name dname), length tvars, NoSyn);
     fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
     val thy'' = thy''' |> Sign.add_types     (map thy_type  dtnvs)
 		       |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
     val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
     val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';

           let val c = hd (Symbol.explode (NameSpace.base_name id))
           in if Symbol.is_letter c then c else "t" end
       | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
       | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
     fun one_con (con,mx,args) =
-	((Syntax.const_name con mx),
+	((Syntax.const_name mx con),
 	 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
 					find_index_eq tp dts,
 					DatatypeAux.dtyp_of_typ new_dts tp),
 					sel,vn))
 	     (args,(mk_var_names(map (typid o third) args)))