--- a/src/Pure/display.ML Sat Oct 24 19:04:57 2009 +0200
+++ b/src/Pure/display.ML Sat Oct 24 19:20:03 2009 +0200
@@ -146,14 +146,14 @@
[Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
val tfrees = map (fn v => TFree (v, []));
- fun pretty_type syn (t, ((Type.LogicalType n, _), _)) =
+ 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))))
- | pretty_type syn (t, ((Type.Abbreviation (vs, U, syn'), _), _)) =
+ | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
if syn <> syn' then NONE
else SOME (Pretty.block
[prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
- | pretty_type syn (t, ((Type.Nonterminal, _), _)) =
+ | pretty_type syn (t, (Type.Nonterminal, _)) =
if not syn then NONE
else SOME (prt_typ (Type (t, [])));