# HG changeset patch
# User wenzelm
# Date 1003766512 -7200
# Node ID 9a9da7969517ecedeb6f5742ce56956f735a4761
# Parent  36d0585f87de72a4cd23512d8cb6ad92c75181bd
Display.print_goals;

diff -r 36d0585f87de -r 9a9da7969517 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Mon Oct 22 18:01:38 2001 +0200
+++ b/src/Pure/tctical.ML	Mon Oct 22 18:01:52 2001 +0200
@@ -198,7 +198,7 @@
 fun print_tac msg = 
     (fn st => 
      (writeln msg;
-      print_goals (!goals_limit) st; Seq.single st));
+      Display.print_goals (!goals_limit) st; Seq.single st));
 
 (*Pause until a line is typed -- if non-empty then fail. *)
 fun pause_tac st =  
@@ -235,7 +235,7 @@
 (*Extract from a tactic, a thm->thm seq function that handles tracing*)
 fun tracify flag tac st =
   if !flag andalso not (!suppress_tracing)
-           then (print_goals (!goals_limit) st;
+           then (Display.print_goals (!goals_limit) st;
                  writeln "** Press RETURN to continue:";
                  exec_trace_command flag (tac,st))
   else tac st;