print_tac now outputs goals through trace-channel
authorschirmer
Tue, 06 Jul 2004 20:32:20 +0200
changeset 15017 9ad392226da5
parent 15016 bcbef8418da5
child 15018 0a84ca4e0f90
print_tac now outputs goals through trace-channel
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 =