--- 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
--- 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));