src/Pure/old_goals.ML
changeset 32089 568a23753e3a
parent 29606 fedb8be05f24
child 32091 30e2ffbba718
     1.1 --- a/src/Pure/old_goals.ML	Mon Jul 20 20:03:19 2009 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Mon Jul 20 21:20:09 2009 +0200
     1.3 @@ -135,7 +135,7 @@
     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.pretty_goals (!goals_limit) state @
     1.8 +  Pretty.str "Bad final proof state:" :: Display_Goal.pretty_goals (!goals_limit) state @
     1.9      [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
    1.10  
    1.11  val result_error_fn = ref result_error_default;
    1.12 @@ -277,7 +277,7 @@
    1.13        (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
    1.14          (if ngoals <> 1 then "s" else "") ^ ")"
    1.15        else ""))] @
    1.16 -    Display.pretty_goals m th
    1.17 +    Display_Goal.pretty_goals m th
    1.18    end |> Pretty.chunks |> Pretty.writeln;
    1.19  
    1.20  (*Printing can raise exceptions, so the assignment occurs last.