# HG changeset patch
# User wenzelm
# Date 1248131110 -7200
# Node ID 6a599543826625c8f3a2e49386ac7bc25ddfaa9c
# Parent  30e2ffbba718a21e7faf7d23646366d1c5a5ae5a
Display.pretty_thm now requires a proper context;

diff -r 30e2ffbba718 -r 6a5995438266 NEWS
--- a/NEWS	Tue Jul 21 01:03:18 2009 +0200
+++ b/NEWS	Tue Jul 21 01:05:10 2009 +0200
@@ -120,6 +120,11 @@
 cominators for "args".  INCOMPATIBILITY, need to use simplified
 Attrib/Method.setup introduced in Isabelle2009.
 
+* Display.pretty_thm now requires a proper context (cf. former
+ProofContext.pretty_thm).  May fall back on Display.pretty_thm_global
+or even Display.pretty_thm_without_context as last resort.
+INCOMPATIBILITY.
+
 
 *** System ***