src/Pure/display.ML
changeset 7067 601f930d3739
parent 6976 3895ba31db71
child 7635 4c1d2eb68db8
     1.1 --- a/src/Pure/display.ML	Fri Jul 23 16:50:20 1999 +0200
     1.2 +++ b/src/Pure/display.ML	Fri Jul 23 16:50:55 1999 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4        [Pretty.str "default:", Pretty.brk 1, prt_sort S];
     1.5  
     1.6      fun pretty_ty (t, n) = Pretty.block
     1.7 -      [Pretty.str (Sign.cond_extern sg Sign.typeK t), Pretty.spc 1, Pretty.str (string_of_int n)];
     1.8 +      [Pretty.str t, Pretty.spc 1, Pretty.str (string_of_int n)];
     1.9  
    1.10      fun pretty_abbr (t, (vs, rhs)) = Pretty.block
    1.11        [prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
    1.12 @@ -189,8 +189,9 @@
    1.13  
    1.14      val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg;
    1.15      val spaces' = Library.sort_wrt fst spaces;
    1.16 -    val {classes, classrel, default, tycons, abbrs, arities} =
    1.17 +    val {classes, classrel, default, tycons = type_tab, abbrs, arities} =
    1.18        Type.rep_tsig tsig;
    1.19 +    val tycons = Sign.cond_extern_table sg Sign.typeK type_tab;
    1.20      val consts = Sign.cond_extern_table sg Sign.constK const_tab;
    1.21    in
    1.22      Pretty.writeln (Pretty.strs ("stamps:" :: Sign.stamp_names_of sg));
    1.23 @@ -198,11 +199,11 @@
    1.24      Pretty.writeln (Pretty.strs ["name prefix:", NameSpace.pack path]);
    1.25      Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_name_space spaces'));
    1.26      Pretty.writeln (pretty_classes classes);
    1.27 -    Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel classrel));
    1.28 +    Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel (Symtab.dest classrel)));
    1.29      Pretty.writeln (pretty_default default);
    1.30      Pretty.writeln (Pretty.big_list "type constructors:" (map pretty_ty tycons));
    1.31 -    Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr abbrs));
    1.32 -    Pretty.writeln (Pretty.big_list "type arities:" (flat (map pretty_arities arities)));
    1.33 +    Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)));
    1.34 +    Pretty.writeln (Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))));
    1.35      Pretty.writeln (Pretty.big_list "consts:" (map pretty_const consts))
    1.36    end;
    1.37