src/Pure/old_goals.ML
changeset 32145 220c9e439d39
parent 32091 30e2ffbba718
child 32173 34f7b0fbe047
     1.1 --- a/src/Pure/old_goals.ML	Thu Jul 23 16:43:31 2009 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Thu Jul 23 16:52:16 2009 +0200
     1.3 @@ -135,7 +135,8 @@
     1.4  (*Default action is to print an error message; could be suppressed for
     1.5    special applications.*)
     1.6  fun result_error_default state msg : thm =
     1.7 -  Pretty.str "Bad final proof state:" :: Display_Goal.pretty_goals (!goals_limit) state @
     1.8 +  Pretty.str "Bad final proof state:" ::
     1.9 +      Display_Goal.pretty_goals_without_context (!goals_limit) state @
    1.10      [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
    1.11  
    1.12  val result_error_fn = ref result_error_default;
    1.13 @@ -277,7 +278,7 @@
    1.14        (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
    1.15          (if ngoals <> 1 then "s" else "") ^ ")"
    1.16        else ""))] @
    1.17 -    Display_Goal.pretty_goals m th
    1.18 +    Display_Goal.pretty_goals_without_context m th
    1.19    end |> Pretty.chunks |> Pretty.writeln;
    1.20  
    1.21  (*Printing can raise exceptions, so the assignment occurs last.