# HG changeset patch # User wenzelm # Date 1167409489 -3600 # Node ID e5c96bb582525a0f65cca09fcc6b8fb3508eaa78 # Parent 4ba9531c60ebf6c15bf4531f0275037a2519082c replaced Sign.classes by Sign.all_classes (topologically sorted); prefer structure Sign over Sorts; renamed Sorts.project to Sorts.subalgebra; diff -r 4ba9531c60eb -r e5c96bb58252 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 =