# 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;