src/Pure/Syntax/mixfix.ML
changeset 26291 d01bf7b10c75
parent 25074 78fdb4c44939
child 29565 3f8b24fcfbd6
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Sat Mar 15 22:07:31 2008 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Sat Mar 15 22:07:32 2008 +0100
     1.3 @@ -104,7 +104,7 @@
     1.4  
     1.5  val strip_esc = implode o strip o Symbol.explode;
     1.6  
     1.7 -fun deprecated c = (legacy_feature ("unnamed infix operator " ^ quote c); c);
     1.8 +fun deprecated c = (legacy_feature ("Unnamed infix operator " ^ quote c); c);
     1.9  
    1.10  fun type_name t (InfixName _) = t
    1.11    | type_name t (InfixlName _) = t