# HG changeset patch
# User wenzelm
# Date 1397039582 -7200
# Node ID 1f660d858a75dbc06837c75a4f8df3e8a888b5cd
# Parent  29a1d14b944ca343e730439cdf6803b53b2b6386
prefer regular Goal_Display.pretty_goals, without censorship of options;

diff -r 29a1d14b944c -r 1f660d858a75 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Wed Apr 09 12:28:24 2014 +0200
+++ b/src/Pure/goal_display.ML	Wed Apr 09 12:33:02 2014 +0200
@@ -15,7 +15,6 @@
   val show_consts: bool Config.T
   val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   val pretty_goals: Proof.context -> thm -> Pretty.T list
-  val pretty_goals_without_context: thm -> Pretty.T list
   val pretty_goal: Proof.context -> thm -> Pretty.T
   val string_of_goal: Proof.context -> thm -> string
 end;
@@ -131,11 +130,6 @@
     (if show_sorts0 then pretty_varsT prop else [])
   end;
 
-fun pretty_goals_without_context th =
-  let val ctxt =
-    Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
-  in pretty_goals ctxt th end;
-
 val pretty_goal = Pretty.chunks oo pretty_goals;
 val string_of_goal = Pretty.string_of oo pretty_goal;
 
diff -r 29a1d14b944c -r 1f660d858a75 src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Wed Apr 09 12:28:24 2014 +0200
+++ b/src/Pure/tactical.ML	Wed Apr 09 12:33:02 2014 +0200
@@ -222,7 +222,7 @@
 fun tracify flag tac st =
   if !flag andalso not (!suppress_tracing) then
     (tracing (Pretty.string_of (Pretty.chunks
-        (Goal_Display.pretty_goals_without_context st @
+        (Goal_Display.pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm st)) st @
           [Pretty.str "** Press RETURN to continue:"])));
      exec_trace_command flag (tac, st))
   else tac st;