replaced Sign.classes by Sign.all_classes (topologically sorted);
authorwenzelm
Fri, 29 Dec 2006 17:24:49 +0100
changeset 21938 e5c96bb58252
parent 21937 4ba9531c60eb
child 21939 9b772ac66830
replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts; renamed Sorts.project to Sorts.subalgebra;
src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Fri Dec 29 17:24:49 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Fri Dec 29 17:24:49 2006 +0100
@@ -566,16 +566,15 @@
 
 fun operational_algebra thy =
   let
-    val algebra = Sign.classes_of thy;
     fun add_iff_operational class classes =
       if (not o null o these o Option.map #params o try (AxClass.get_definition thy)) class
         orelse (length o gen_inter (op =))
           ((Sign.certify_sort thy o Sign.super_classes thy) class, classes) >= 2
       then class :: classes
       else classes;
-    val operational_classes = fold add_iff_operational (Sorts.classes algebra) [];
+    val operational_classes = fold add_iff_operational (Sign.all_classes thy) [];
   in
-    Sorts.project_algebra (Sign.pp thy) (member (op =) operational_classes) algebra
+    Sorts.subalgebra (Sign.pp thy) (member (op =) operational_classes) (Sign.classes_of thy)
   end;
 
 fun generate thy funcgr targets init gen it =