changeset 24928 | 3419943838f5 |
parent 24848 | 5dbbd33c3236 |
child 24969 | b38527eefb3b |
--- 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;