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 ""