deprecated old-style infix declarations, which mix name and syntax;

--- a/src/Pure/Syntax/mixfix.ML	Tue Sep 06 16:59:58 2005 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Tue Sep 06 16:59:59 2005 +0200
@@ -97,25 +97,27 @@
 
 val strip_esc = implode o strip o Symbol.explode;
 
+fun deprecated c = (warning ("Unnamed infix operator " ^ quote c ^ " -- deprecated"); c);
+
 fun type_name t (InfixName _) = t
   | type_name t (InfixlName _) = t
   | type_name t (InfixrName _) = t
-  | type_name t (Infix _) = strip_esc t
-  | type_name t (Infixl _) = strip_esc t
-  | type_name t (Infixr _) = strip_esc t
+  | type_name t (Infix _) = deprecated (strip_esc t)
+  | type_name t (Infixl _) = deprecated (strip_esc t)
+  | type_name t (Infixr _) = deprecated (strip_esc t)
   | type_name t _ = t;
 
 fun const_name c (InfixName _) = c
   | const_name c (InfixlName _) = c
   | const_name c (InfixrName _) = c
-  | const_name c (Infix _) = "op " ^ strip_esc c
-  | const_name c (Infixl _) = "op " ^ strip_esc c
-  | const_name c (Infixr _) = "op " ^ strip_esc c
+  | const_name c (Infix _) = "op " ^ deprecated (strip_esc c)
+  | const_name c (Infixl _) = "op " ^ deprecated (strip_esc c)
+  | const_name c (Infixr _) = "op " ^ deprecated (strip_esc c)
   | const_name c _ = c;
 
-fun fix_mixfix c (Infix p) = (InfixName (c, p))
-  | fix_mixfix c (Infixl p) = (InfixlName (c, p))
-  | fix_mixfix c (Infixr p) = (InfixrName (c, p))
+fun fix_mixfix c (Infix p) = (deprecated (strip_esc c); InfixName (c, p))
+  | fix_mixfix c (Infixl p) = (deprecated (strip_esc c); InfixlName (c, p))
+  | fix_mixfix c (Infixr p) = (deprecated (strip_esc c); InfixrName (c, p))
   | fix_mixfix _ mx = mx;
 
 fun mixfix_args NoSyn = 0