--- a/src/Pure/display.ML Wed Jun 08 22:16:21 2011 +0200
+++ b/src/Pure/display.ML Thu Jun 09 20:22:22 2011 +0200
@@ -156,7 +156,7 @@
val tfrees = map (fn v => TFree (v, []));
fun pretty_type syn (t, (Type.LogicalType n)) =
if syn then NONE
- else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
+ else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
| pretty_type syn (t, (Type.Abbreviation (vs, U, syn'))) =
if syn <> syn' then NONE
else SOME (Pretty.block