# HG changeset patch
# User haftmann
# Date 1272435902 -7200
# Node ID 06081e4921d618fe374022c4ed0988d35408b22c
# Parent  0685b4336132dbf1441ea4d8a79212754918afc1
term_typ: print styled term

diff -r 0685b4336132 -r 06081e4921d6 NEWS
--- a/NEWS	Tue Apr 27 22:23:12 2010 +0200
+++ b/NEWS	Wed Apr 28 08:25:02 2010 +0200
@@ -84,6 +84,8 @@
 
 *** Pure ***
 
+* Old 'axclass' has been discontinued.  Use 'class' instead.  INCOMPATIBILITY.
+
 * Code generator: simple concept for abstract datatypes obeying invariants.
 
 * Local theory specifications may depend on extra type variables that
diff -r 0685b4336132 -r 06081e4921d6 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Apr 27 22:23:12 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Wed Apr 28 08:25:02 2010 +0200
@@ -453,7 +453,7 @@
 
 fun pretty_term_typ ctxt (style, t) =
   let val t' = style t
-  in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t) end;
+  in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t') t') end;
 
 fun pretty_term_typeof ctxt (style, t) =
   Syntax.pretty_typ ctxt (Term.fastype_of (style t));