src/Pure/Isar/generic_target.ML
changeset 38831 4933a3dfd745
parent 38757 2b3e054ae6fc
child 39557 fe5722fce758
--- a/src/Pure/Isar/generic_target.ML	Fri Aug 27 18:00:45 2010 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Aug 27 19:43:28 2010 +0200
@@ -41,7 +41,7 @@
 fun check_mixfix ctxt (b, extra_tfrees) mx =
   if null extra_tfrees then mx
   else
-    (warning
+    (Context_Position.if_visible ctxt warning
       ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
         commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
         (if mx = NoSyn then ""