1.1 --- a/src/Pure/goal_display.ML	Wed Apr 09 12:28:24 2014 +0200
     1.2 +++ b/src/Pure/goal_display.ML	Wed Apr 09 12:33:02 2014 +0200
     1.3 @@ -15,7 +15,6 @@
     1.4    val show_consts: bool Config.T
     1.5    val pretty_flexpair: Proof.context -> term * term -> Pretty.T
     1.6    val pretty_goals: Proof.context -> thm -> Pretty.T list
     1.7 -  val pretty_goals_without_context: thm -> Pretty.T list
     1.8    val pretty_goal: Proof.context -> thm -> Pretty.T
     1.9    val string_of_goal: Proof.context -> thm -> string
    1.10  end;
    1.11 @@ -131,11 +130,6 @@
    1.12      (if show_sorts0 then pretty_varsT prop else [])
    1.13    end;
    1.14  
    1.15 -fun pretty_goals_without_context th =
    1.16 -  let val ctxt =
    1.17 -    Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
    1.18 -  in pretty_goals ctxt th end;
    1.19 -
    1.20  val pretty_goal = Pretty.chunks oo pretty_goals;
    1.21  val string_of_goal = Pretty.string_of oo pretty_goal;
    1.22  

     2.1 --- a/src/Pure/tactical.ML	Wed Apr 09 12:28:24 2014 +0200
     2.2 +++ b/src/Pure/tactical.ML	Wed Apr 09 12:33:02 2014 +0200
     2.3 @@ -222,7 +222,7 @@
     2.4  fun tracify flag tac st =
     2.5    if !flag andalso not (!suppress_tracing) then
     2.6      (tracing (Pretty.string_of (Pretty.chunks
     2.7 -        (Goal_Display.pretty_goals_without_context st @
     2.8 +        (Goal_Display.pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm st)) st @
     2.9            [Pretty.str "** Press RETURN to continue:"])));
    2.10       exec_trace_command flag (tac, st))
    2.11    else tac st;