eliminated print_goals_without_context -- proper pretty printing;

--- a/src/Pure/display_goal.ML	Fri Jul 24 11:50:35 2009 +0200
+++ b/src/Pure/display_goal.ML	Fri Jul 24 11:55:34 2009 +0200
@@ -13,7 +13,6 @@
   val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
     thm -> Pretty.T list
   val pretty_goals_without_context: int -> thm -> Pretty.T list
-  val print_goals_without_context: int -> thm -> unit
 end;
 
 structure Display_Goal: DISPLAY_GOAL =
@@ -119,9 +118,6 @@
   pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th))
     {total = true, main = true, maxgoals = n} th;
 
-val print_goals_without_context =
-  (Pretty.writeln o Pretty.chunks) oo pretty_goals_without_context;
-
 end;
 
 end;

--- a/src/Pure/tctical.ML	Fri Jul 24 11:50:35 2009 +0200
+++ b/src/Pure/tctical.ML	Fri Jul 24 11:55:34 2009 +0200
@@ -232,9 +232,10 @@
 (*Extract from a tactic, a thm->thm seq function that handles tracing*)
 fun tracify flag tac st =
   if !flag andalso not (!suppress_tracing) then
-   (Display_Goal.print_goals_without_context (! Display_Goal.goals_limit) st;
-    tracing "** Press RETURN to continue:";
-    exec_trace_command flag (tac, st))
+    (tracing (Pretty.string_of (Pretty.chunks
+        (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st @
+          [Pretty.str "** Press RETURN to continue:"])));
+     exec_trace_command flag (tac, st))
   else tac st;
 
 (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)