src/HOL/Tools/Datatype/datatype_aux.ML

   | mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]);
 
 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 _ = "";
 
 fun dtyp_of_typ _ (TFree (n, _)) = DtTFree n
   | dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"