# HG changeset patch # User haftmann # Date 1181049369 -7200 # Node ID ef04b4c12593157a7fdaacfcb3439dc337d29f7d # Parent b99dce43d252853acb9f91ddb8d100ed62390d39 simplified notion of "operational classes" diff -r b99dce43d252 -r ef04b4c12593 src/Pure/Tools/codegen_data.ML --- a/src/Pure/Tools/codegen_data.ML Tue Jun 05 15:16:08 2007 +0200 +++ b/src/Pure/Tools/codegen_data.ML Tue Jun 05 15:16:09 2007 +0200 @@ -549,12 +549,8 @@ fun coregular_algebra thy = retrieve_algebra thy (K true) |> snd; fun operational_algebra thy = let - 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; + fun add_iff_operational class = + can (AxClass.get_definition thy) class ? cons class; val operational_classes = fold add_iff_operational (Sign.all_classes thy) [] in retrieve_algebra thy (member (op =) operational_classes) end;