# HG changeset patch
# User schirmer
# Date 1089138740 -7200
# Node ID 9ad392226da54cb4cf866652f39ab05c78b52150
# Parent  bcbef8418da506db4bd9675beb40e931f735fe45
print_tac now outputs goals through trace-channel

diff -r bcbef8418da5 -r 9ad392226da5 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Tue Jul 06 20:31:37 2004 +0200
+++ b/src/Pure/tctical.ML	Tue Jul 06 20:32:20 2004 +0200
@@ -198,7 +198,9 @@
 fun print_tac msg =
     (fn st =>
      (tracing msg;
-      Display.print_goals (! Display.goals_limit) st; Seq.single st));
+      tracing ((Pretty.string_of o Pretty.chunks o 
+                 Display.pretty_goals (! Display.goals_limit)) st); 
+      Seq.single st));
 
 (*Pause until a line is typed -- if non-empty then fail. *)
 fun pause_tac st =