--- a/src/Pure/Tools/find_theorems.ML Mon Sep 21 21:46:14 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML Mon Sep 21 23:22:11 2015 +0200
@@ -551,7 +551,7 @@
val _ =
Query_Operation.register {name = "find_theorems", pri = Task_Queue.urgent_pri}
- (fn {state = st, args, output_result} =>
+ (fn {state = st, args, writeln_result, ...} =>
if can Toplevel.context_of st then
let
val [limit_arg, allow_dups_arg, query_arg] = args;
@@ -559,7 +559,7 @@
val opt_limit = Int.fromString limit_arg;
val rem_dups = allow_dups_arg = "false";
val criteria = read_query Position.none query_arg;
- in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
+ in writeln_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
else error "Unknown context");
end;