equal
deleted
inserted
replaced
40 else |
40 else |
41 (Context_Position.if_visible ctxt warning |
41 (Context_Position.if_visible ctxt warning |
42 ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^ |
42 ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^ |
43 commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^ |
43 commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^ |
44 (if mx = NoSyn then "" |
44 (if mx = NoSyn then "" |
45 else "\nDropping mixfix syntax " ^ Pretty.string_of (Syntax.pretty_mixfix mx))); |
45 else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))); |
46 NoSyn); |
46 NoSyn); |
47 |
47 |
48 |
48 |
49 (* define *) |
49 (* define *) |
50 |
50 |