diff -r 48e08f37ce92 -r 3419943838f5 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Oct 09 17:10:36 2007 +0200
+++ b/src/Pure/Isar/code.ML	Tue Oct 09 17:10:38 2007 +0200
@@ -597,7 +597,7 @@
 fun operational_algebra thy =
   let
     fun add_iff_operational class =
-      can (AxClass.get_definition thy) class ? cons class;
+      can (AxClass.get_info thy) class ? cons class;
     val operational_classes = fold add_iff_operational (Sign.all_classes thy) []
   in retrieve_algebra thy (member (op =) operational_classes) end;