src/Pure/Tools/find_consts.ML
changeset 61223 dfccf6c06201
parent 60667 d86c449d30ba
child 61335 43848476063c
     1.1 --- a/src/Pure/Tools/find_consts.ML	Mon Sep 21 21:46:14 2015 +0200
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Sep 21 23:22:11 2015 +0200
     1.3 @@ -165,13 +165,13 @@
     1.4  
     1.5  val _ =
     1.6    Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri}
     1.7 -    (fn {state, args, output_result} =>
     1.8 +    (fn {state, args, writeln_result, ...} =>
     1.9        (case try Toplevel.context_of state of
    1.10          SOME ctxt =>
    1.11            let
    1.12              val [query_arg] = args;
    1.13              val query = read_query Position.none query_arg;
    1.14 -          in output_result (Pretty.string_of (pretty_consts ctxt query)) end
    1.15 +          in writeln_result (Pretty.string_of (pretty_consts ctxt query)) end
    1.16        | NONE => error "Unknown context"));
    1.17  
    1.18  end;