src/Pure/display.ML
changeset 33092 c859019d3ac5
parent 32784 1a5dde5079ac
child 33095 bbd52d2f8696
     1.1 --- a/src/Pure/display.ML	Sat Oct 24 19:04:57 2009 +0200
     1.2 +++ b/src/Pure/display.ML	Sat Oct 24 19:20:03 2009 +0200
     1.3 @@ -146,14 +146,14 @@
     1.4        [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
     1.5  
     1.6      val tfrees = map (fn v => TFree (v, []));
     1.7 -    fun pretty_type syn (t, ((Type.LogicalType n, _), _)) =
     1.8 +    fun pretty_type syn (t, (Type.LogicalType n, _)) =
     1.9            if syn then NONE
    1.10            else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
    1.11 -      | pretty_type syn (t, ((Type.Abbreviation (vs, U, syn'), _), _)) =
    1.12 +      | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
    1.13            if syn <> syn' then NONE
    1.14            else SOME (Pretty.block
    1.15              [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
    1.16 -      | pretty_type syn (t, ((Type.Nonterminal, _), _)) =
    1.17 +      | pretty_type syn (t, (Type.Nonterminal, _)) =
    1.18            if not syn then NONE
    1.19            else SOME (prt_typ (Type (t, [])));
    1.20