replaced Sign.classes by Sign.all_classes (topologically sorted);
authorwenzelm
Fri, 29 Dec 2006 17:24:47 +0100
changeset 21936 c7a7d3ab81d0
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
--- a/src/Pure/Tools/class_package.ML	Fri Dec 29 17:24:46 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Dec 29 17:24:47 2006 +0100
@@ -121,7 +121,7 @@
     fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
       (SOME o Pretty.str) ("class " ^ class ^ ":"),
       (SOME o Pretty.block) [Pretty.str "supersort: ",
-        (Sign.pretty_sort thy o Sorts.certify_sort algebra o Sorts.super_classes algebra) class],
+        (Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class],
       Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
       ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
         o these o Option.map #params o try (AxClass.get_definition thy)) class,
@@ -131,7 +131,8 @@
       ]
     ]
   in
-    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.classes) algebra
+    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.all_classes)
+      algebra
   end;