src/HOL/Tools/Datatype/datatype_aux.ML

--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Apr 08 16:34:14 2011 +0200
@@ -232,7 +232,7 @@
 fun name_of_typ (Type (s, Ts)) =
       let val s' = Long_Name.base_name s
       in space_implode "_" (filter_out (equal "") (map name_of_typ Ts) @
-        [if Syntax.is_identifier s' then s' else "x"])
+        [if Lexicon.is_identifier s' then s' else "x"])
       end
   | name_of_typ _ = "";