src/Tools/try.ML
changeset 52647 45ce95b8bf69
parent 52645 e8c1c5612677
child 52648 b1ae4306f29f
--- a/src/Tools/try.ML	Sat Jul 13 14:13:34 2013 +0200
+++ b/src/Tools/try.ML	Sat Jul 13 16:34:57 2013 +0200
@@ -116,10 +116,10 @@
 (* asynchronous print function (PIDE) *)
 
 fun print_function ((name, (weight, auto, tool)): tool) =
-  Command.print_function {name = name, pri = ~ weight, persistent = true}
+  Command.print_function name
     (fn {command_name} =>
       if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
-        SOME (fn _ => fn st =>
+        SOME {pri = ~ weight, persistent = true, print_fn = fn _ => fn st =>
           let
             val auto_time_limit = Options.default_real @{option auto_time_limit}
           in
@@ -134,7 +134,7 @@
                   | _ => ())
               | NONE => ())
             else ()
-          end)
+          end}
       else NONE);