| changeset 20664 | ffbc5a57191a |
| parent 19265 | cae36e16f3c0 |
| child 20926 | b2f67b947200 |
--- a/src/Pure/General/output.ML Thu Sep 21 19:04:12 2006 +0200 +++ b/src/Pure/General/output.ML Thu Sep 21 19:04:20 2006 +0200 @@ -67,7 +67,7 @@ val print_mode = ref ([]: string list); -fun has_mode s = s mem_string ! print_mode; +fun has_mode s = member (op =) (! print_mode) s; type mode_fns = {output: string -> string * real,