src/Pure/sorts.ML
changeset 44338 700008399ee5
parent 43792 d5803c3d537a
child 45595 fe57d786fd5b
     1.1 --- a/src/Pure/sorts.ML	Sat Aug 20 22:46:19 2011 +0200
     1.2 +++ b/src/Pure/sorts.ML	Sat Aug 20 23:35:30 2011 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4  
     1.5  fun all_classes (Algebra {classes, ...}) = Graph.all_preds classes (Graph.maximals classes);
     1.6  
     1.7 -val super_classes = Graph.imm_succs o classes_of;
     1.8 +val super_classes = Graph.immediate_succs o classes_of;
     1.9  
    1.10  
    1.11  (* class relations *)
    1.12 @@ -413,7 +413,7 @@
    1.13        end;
    1.14  
    1.15      fun derive (_, []) = []
    1.16 -      | derive (T as Type (a, Us), S) =
    1.17 +      | derive (Type (a, Us), S) =
    1.18            let
    1.19              val Ss = mg_domain algebra a S;
    1.20              val dom = map2 (fn U => fn S => derive (U, S) ~~ S) Us Ss;