changeset 30364 | 577edc39b501 |
parent 30280 | eb98b49ef835 |
--- a/src/HOL/Tools/datatype_aux.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/datatype_aux.ML Sun Mar 08 17:26:14 2009 +0100 @@ -224,7 +224,7 @@ | mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]); fun name_of_typ (Type (s, Ts)) = - let val s' = NameSpace.base_name s + let val s' = Long_Name.base_name s in space_implode "_" (List.filter (not o equal "") (map name_of_typ Ts) @ [if Syntax.is_identifier s' then s' else "x"]) end