src/Pure/old_goals.ML
changeset 32091 30e2ffbba718
parent 32089 568a23753e3a
child 32145 220c9e439d39
--- a/src/Pure/old_goals.ML	Tue Jul 21 00:56:19 2009 +0200
+++ b/src/Pure/old_goals.ML	Tue Jul 21 01:03:18 2009 +0200
@@ -199,7 +199,7 @@
   case e of
      THM (msg,i,thms) =>
          (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
-          List.app Display.print_thm thms)
+          List.app (writeln o Display.string_of_thm_global thy) thms)
    | THEORY (msg,thys) =>
          (writeln ("Exception THEORY raised:\n" ^ msg);
           List.app (writeln o Context.str_of_thy) thys)