simplified notion of "operational classes"
authorhaftmann
Tue, 05 Jun 2007 15:16:09 +0200
changeset 23248 ef04b4c12593
parent 23247 b99dce43d252
child 23249 9ef65be6bb2a
simplified notion of "operational classes"
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;