diff -r bcee022fbe30 -r abd3885a3fcf src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Thu Apr 24 21:39:40 2025 +0200 +++ b/src/Pure/Tools/find_theorems.ML Thu Apr 24 22:45:04 2025 +0200 @@ -536,7 +536,7 @@ val _ = Query_Operation.register {name = "find_theorems", pri = Task_Queue.urgent_pri} - (fn {state = st, args, writeln_result, ...} => + (fn {state = st, args, writelns_result, ...} => if can Toplevel.context_of st then let val [limit_arg, allow_dups_arg, query_arg] = args; @@ -544,7 +544,7 @@ val opt_limit = Int.fromString limit_arg; val rem_dups = allow_dups_arg = "false"; val criteria = read_query Position.none query_arg; - in writeln_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end + in writelns_result (Pretty.strings_of (pretty_theorems state opt_limit rem_dups criteria)) end else error "Unknown context"); end;