src/HOL/Tools/datatype_aux.ML
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