src/ZF/thy_syntax.ML
changeset 6093 87bf8c03b169
parent 6070 032babd0120b
child 6112 5e4871c5136b
     1.1 --- a/src/ZF/thy_syntax.ML	Tue Jan 12 13:54:51 1999 +0100
     1.2 +++ b/src/ZF/thy_syntax.ML	Tue Jan 12 15:17:37 1999 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  (*ML identifiers for introduction rules.*)
     1.6  fun mk_intr_name suffix s =  
     1.7 -    if Syntax.is_identifier s then
     1.8 +    if ThmDatabase.is_ml_identifier s then
     1.9  	"op " ^ s ^ suffix  (*the "op" cancels any infix status*)
    1.10      else "_";               (*bad name, don't try to bind*)
    1.11