src/ZF/thy_syntax.ML

--- a/src/ZF/thy_syntax.ML	Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/thy_syntax.ML	Tue Jan 12 15:17:37 1999 +0100
@@ -14,7 +14,7 @@
 
 (*ML identifiers for introduction rules.*)
 fun mk_intr_name suffix s =  
-    if Syntax.is_identifier s then
+    if ThmDatabase.is_ml_identifier s then
 	"op " ^ s ^ suffix  (*the "op" cancels any infix status*)
     else "_";               (*bad name, don't try to bind*)