src/Pure/Isar/code.ML
changeset 24731 c25aa6ae64ec
parent 24659 6b7ac2a43df8
child 24837 cacc5744be75
     1.1 --- a/src/Pure/Isar/code.ML	Wed Sep 26 20:27:58 2007 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Wed Sep 26 20:50:33 2007 +0200
     1.3 @@ -541,7 +541,7 @@
     1.4  
     1.5  fun weakest_constraints thy (class, tyco) =
     1.6    let
     1.7 -    val all_superclasses = class :: Graph.all_succs ((#classes o Sorts.rep_algebra o Sign.classes_of) thy) [class];
     1.8 +    val all_superclasses = Sign.complete_sort thy [class];
     1.9    in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses)
    1.10     of SOME sorts => sorts
    1.11      | NONE => Sign.arity_sorts thy tyco [class]
    1.12 @@ -555,7 +555,7 @@
    1.13    in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses)
    1.14     of SOME sorts => sorts
    1.15      | NONE => replicate
    1.16 -        (Sign.arity_number thy tyco) (Sign.certify_sort thy (Sign.all_classes thy))
    1.17 +        (Sign.arity_number thy tyco) (Sign.minimize_sort thy (Sign.all_classes thy))
    1.18    end;
    1.19  
    1.20  fun gen_classop_typ constr thy class (c, tyco) =