src/Pure/display.ML
changeset 15000 3d6245229e48
parent 14996 2571227f3fcc
child 15531 08c8dad8e399
     1.1 --- a/src/Pure/display.ML	Tue Jun 22 14:14:08 2004 +0200
     1.2 +++ b/src/Pure/display.ML	Wed Jun 23 09:09:18 2004 +0200
     1.3 @@ -199,14 +199,14 @@
     1.4              prt_typ_no_tvars T, Pretty.str " ::", 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 (Term.invent_names [] "'a" 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  
    1.21 @@ -229,9 +229,8 @@
    1.22      val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
    1.23  
    1.24      val spcs = Library.sort_wrt #1 spaces;
    1.25 -    val tdecls =
    1.26 -      map (apfst (fn t => (Sign.cond_extern sg Sign.typeK t, t))) (Symtab.dest types)
    1.27 -      |> Library.sort_wrt (#1 o #1);
    1.28 +    val tdecls = Symtab.dest types |> map (fn (t, (d, _)) =>
    1.29 +      (Sign.cond_extern sg Sign.typeK t, (t, d))) |> Library.sort_wrt #1 |> map #2;
    1.30      val cnsts = Sign.cond_extern_table sg Sign.constK consts;
    1.31      val finals = Sign.cond_extern_table sg Sign.constK final_consts;
    1.32      val axms = Sign.cond_extern_table sg Theory.axiomK axioms;