src/Pure/old_goals.ML
changeset 32187 cca43ca13f4f
parent 32179 1c9c991e41c0
child 32231 95b8afcbb0ed
     1.1 --- a/src/Pure/old_goals.ML	Sat Jul 25 00:53:47 2009 +0200
     1.2 +++ b/src/Pure/old_goals.ML	Sat Jul 25 10:31:27 2009 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4    special applications.*)
     1.5  fun result_error_default state msg : thm =
     1.6    Pretty.str "Bad final proof state:" ::
     1.7 -      Display_Goal.pretty_goals_without_context (!goals_limit) state @
     1.8 +      Goal_Display.pretty_goals_without_context (!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 @@ -267,7 +267,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_Goal.pretty_goals_without_context m th
    1.17 +    Goal_Display.pretty_goals_without_context m th
    1.18    end |> Pretty.chunks |> Pretty.writeln;
    1.19  
    1.20  (*Printing can raise exceptions, so the assignment occurs last.