src/Pure/Isar/code.ML
changeset 24928 3419943838f5
parent 24848 5dbbd33c3236
child 24969 b38527eefb3b
     1.1 --- a/src/Pure/Isar/code.ML	Tue Oct 09 17:10:36 2007 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Oct 09 17:10:38 2007 +0200
     1.3 @@ -597,7 +597,7 @@
     1.4  fun operational_algebra thy =
     1.5    let
     1.6      fun add_iff_operational class =
     1.7 -      can (AxClass.get_definition thy) class ? cons class;
     1.8 +      can (AxClass.get_info thy) class ? cons class;
     1.9      val operational_classes = fold add_iff_operational (Sign.all_classes thy) []
    1.10    in retrieve_algebra thy (member (op =) operational_classes) end;
    1.11