replaced Sign.classes by Sign.all_classes (topologically sorted);
authorwenzelm
Fri Dec 29 17:24:47 2006 +0100 (2006-12-29)
changeset 21936c7a7d3ab81d0
parent 21935 4e20a5397b57
child 21937 4ba9531c60eb
replaced Sign.classes by Sign.all_classes (topologically sorted);
prefer structure Sign over Sorts;
src/Pure/Tools/class_package.ML
     1.1 --- a/src/Pure/Tools/class_package.ML	Fri Dec 29 17:24:46 2006 +0100
     1.2 +++ b/src/Pure/Tools/class_package.ML	Fri Dec 29 17:24:47 2006 +0100
     1.3 @@ -121,7 +121,7 @@
     1.4      fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
     1.5        (SOME o Pretty.str) ("class " ^ class ^ ":"),
     1.6        (SOME o Pretty.block) [Pretty.str "supersort: ",
     1.7 -        (Sign.pretty_sort thy o Sorts.certify_sort algebra o Sorts.super_classes algebra) class],
     1.8 +        (Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class],
     1.9        Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
    1.10        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
    1.11          o these o Option.map #params o try (AxClass.get_definition thy)) class,
    1.12 @@ -131,7 +131,8 @@
    1.13        ]
    1.14      ]
    1.15    in
    1.16 -    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.classes) algebra
    1.17 +    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.all_classes)
    1.18 +      algebra
    1.19    end;
    1.20  
    1.21