src/Pure/display.ML
changeset 19482 9f11af8f7ef9
parent 19420 bd5c0adec2b1
child 19521 cfdab6a91332
     1.1 --- a/src/Pure/display.ML	Thu Apr 27 12:11:56 2006 +0200
     1.2 +++ b/src/Pure/display.ML	Thu Apr 27 15:06:35 2006 +0200
     1.3 @@ -188,7 +188,7 @@
     1.4            if not syn then NONE
     1.5            else SOME (prt_typ (Type (t, [])));
     1.6  
     1.7 -    val pretty_arities = List.concat o map (fn (t, ars) => map (prt_arity t) ars);
     1.8 +    val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars);
     1.9  
    1.10      fun pretty_const (c, ty) = Pretty.block
    1.11        [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    1.12 @@ -208,8 +208,8 @@
    1.13      val tdecls = NameSpace.dest_table types;
    1.14      val arties = NameSpace.dest_table (Sign.type_space thy, arities);
    1.15      val cnsts = NameSpace.extern_table constants;
    1.16 -    val log_cnsts = List.mapPartial (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
    1.17 -    val abbrevs = List.mapPartial (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
    1.18 +    val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
    1.19 +    val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
    1.20      val cnstrs = NameSpace.extern_table constraints;
    1.21      val axms = NameSpace.extern_table axioms;
    1.22      val oras = NameSpace.extern_table oracles;
    1.23 @@ -221,8 +221,8 @@
    1.24        Pretty.big_list "classes:" (map pretty_classrel clsses),
    1.25        pretty_default default,
    1.26        pretty_witness witness,
    1.27 -      Pretty.big_list "syntactic types:" (List.mapPartial (pretty_type true) tdecls),
    1.28 -      Pretty.big_list "logical types:" (List.mapPartial (pretty_type false) tdecls),
    1.29 +      Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
    1.30 +      Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),
    1.31        Pretty.big_list "type arities:" (pretty_arities arties),
    1.32        Pretty.big_list "logical consts:" (map pretty_const log_cnsts),
    1.33        Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),