src/Pure/variable.ML

--- a/src/Pure/variable.ML	Fri Aug 27 18:00:45 2010 +0200
+++ b/src/Pure/variable.ML	Fri Aug 27 19:43:28 2010 +0200
@@ -506,7 +506,7 @@
     val tfrees = map #1 extras |> sort_distinct string_ord;
     val frees = map #2 extras |> sort_distinct string_ord;
   in
-    if null extras then ()
+    if null extras orelse not (Context_Position.is_visible ctxt2) then ()
     else warning ("Introduced fixed type variable(s): " ^ commas tfrees ^ " in " ^
       space_implode " or " (map quote frees))
   end;