use ThmDatabase.is_ml_identifier;

--- a/src/HOL/thy_syntax.ML	Mon Apr 26 14:46:47 2004 +0200
+++ b/src/HOL/thy_syntax.ML	Mon Apr 26 14:53:29 2004 +0200
@@ -53,7 +53,7 @@
   let
     val no_atts = map (mk_pair o rpair "[]");
     fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
-      if Syntax.is_identifier s then "op " ^ s else "_";
+      if ThmDatabase.is_ml_identifier s then "op " ^ s else "_";
     fun mk_params ((recs, ipairs), monos) =
       let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs)
           and srec_tms = mk_list recs
@@ -94,7 +94,7 @@
   (*** and bindig theorems to ML identifiers    ***)
 
   fun mk_bind_thms_string names =
-   (case find_first (not o Syntax.is_identifier) names of
+   (case find_first (not o ThmDatabase.is_ml_identifier) names of
       Some id => (warning (id ^ " is not a valid identifier"); "")
     | None =>
         let