src/HOL/Tools/datatype_aux.ML

--- a/src/HOL/Tools/datatype_aux.ML	Mon Apr 26 14:53:29 2004 +0200
+++ b/src/HOL/Tools/datatype_aux.ML	Mon Apr 26 14:54:45 2004 +0200
@@ -227,7 +227,7 @@
 fun name_of_typ (Type (s, Ts)) =
       let val s' = Sign.base_name s
       in space_implode "_" (filter (not o equal "") (map name_of_typ Ts) @
-        [if Symbol.is_identifier s' then s' else "x"])
+        [if Syntax.is_identifier s' then s' else "x"])
       end
   | name_of_typ _ = "";