src/Pure/Tools/find_theorems.ML
changeset 82583 abd3885a3fcf
parent 81729 560a069a537f
--- 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;