src/Pure/display.ML
changeset 24848 5dbbd33c3236
parent 24774 bc31c318e673
child 24920 2a45e400fdad
     1.1 --- a/src/Pure/display.ML	Thu Oct 04 20:29:13 2007 +0200
     1.2 +++ b/src/Pure/display.ML	Thu Oct 04 20:29:24 2007 +0200
     1.3 @@ -172,7 +172,7 @@
     1.4      val tfrees = map (fn v => TFree (v, []));
     1.5      fun pretty_type syn (t, (Type.LogicalType n, _)) =
     1.6            if syn then NONE
     1.7 -          else SOME (prt_typ (Type (t, tfrees (Name.invent_list [] "'a" n))))
     1.8 +          else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
     1.9        | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
    1.10            if syn <> syn' then NONE
    1.11            else SOME (Pretty.block