diff -r bcee022fbe30 -r abd3885a3fcf src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Thu Apr 24 21:39:40 2025 +0200 +++ b/src/Pure/Tools/find_consts.ML Thu Apr 24 22:45:04 2025 +0200 @@ -159,13 +159,13 @@ val _ = Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri} - (fn {state, args, writeln_result, ...} => + (fn {state, args, writelns_result, ...} => (case try Toplevel.context_of state of SOME ctxt => let val [query_arg] = args; val query = read_query Position.none query_arg; - in writeln_result (Pretty.string_of (pretty_consts ctxt query)) end + in writelns_result (Pretty.strings_of (pretty_consts ctxt query)) end | NONE => error "Unknown context")); end;