1.1 --- a/src/Pure/ML/ml_lex.ML	Wed Nov 03 11:33:51 2010 +0100
     1.2 +++ b/src/Pure/ML/ml_lex.ML	Wed Nov 03 13:54:23 2010 +0100
     1.3 @@ -73,7 +73,14 @@
     1.4  fun check_content_of tok =
     1.5    (case kind_of tok of
     1.6      Error msg => error msg
     1.7 -  | _ => content_of tok);
     1.8 +  | _ =>
     1.9 +      (case tok of
    1.10 +        Token (_, (Keyword, ":>")) =>
    1.11 +          warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
    1.12 +            \prefer non-opaque matching (:) possibly with abstype" ^
    1.13 +            Position.str_of (pos_of tok))
    1.14 +      | _ => ();
    1.15 +      content_of tok));
    1.16  
    1.17  val flatten = implode o map (Symbol.escape o check_content_of);
    1.18