--- 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;
--- 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;