--- a/src/Pure/old_goals.ML Thu Jul 23 16:43:31 2009 +0200
+++ b/src/Pure/old_goals.ML Thu Jul 23 16:52:16 2009 +0200
@@ -135,7 +135,8 @@
(*Default action is to print an error message; could be suppressed for
special applications.*)
fun result_error_default state msg : thm =
- Pretty.str "Bad final proof state:" :: Display_Goal.pretty_goals (!goals_limit) state @
+ Pretty.str "Bad final proof state:" ::
+ Display_Goal.pretty_goals_without_context (!goals_limit) state @
[Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
val result_error_fn = ref result_error_default;
@@ -277,7 +278,7 @@
(if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
(if ngoals <> 1 then "s" else "") ^ ")"
else ""))] @
- Display_Goal.pretty_goals m th
+ Display_Goal.pretty_goals_without_context m th
end |> Pretty.chunks |> Pretty.writeln;
(*Printing can raise exceptions, so the assignment occurs last.