src/HOL/thy_syntax.ML
changeset 14672 79bac83b2c27
parent 14598 7009f59711e3
child 14700 2f885b7e5ba7
     1.1 --- a/src/HOL/thy_syntax.ML	Mon Apr 26 14:46:47 2004 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Mon Apr 26 14:53:29 2004 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4    let
     1.5      val no_atts = map (mk_pair o rpair "[]");
     1.6      fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
     1.7 -      if Syntax.is_identifier s then "op " ^ s else "_";
     1.8 +      if ThmDatabase.is_ml_identifier s then "op " ^ s else "_";
     1.9      fun mk_params ((recs, ipairs), monos) =
    1.10        let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs)
    1.11            and srec_tms = mk_list recs
    1.12 @@ -94,7 +94,7 @@
    1.13    (*** and bindig theorems to ML identifiers    ***)
    1.14  
    1.15    fun mk_bind_thms_string names =
    1.16 -   (case find_first (not o Syntax.is_identifier) names of
    1.17 +   (case find_first (not o ThmDatabase.is_ml_identifier) names of
    1.18        Some id => (warning (id ^ " is not a valid identifier"); "")
    1.19      | None =>
    1.20          let