1.1 --- a/src/Pure/type.ML	Thu Feb 01 20:45:11 2001 +0100
     1.2 +++ b/src/Pure/type.ML	Thu Feb 01 20:45:54 2001 +0100
     1.3 @@ -531,7 +531,7 @@
     1.4  fun ext_tsig_classes tsig new_classes =
     1.5    let
     1.6      val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
     1.7 -    val (classes',classrel') = extend_classes (classes,classrel,new_classes);
     1.8 +    val (classes', classrel') = extend_classes (classes,classrel, new_classes);
     1.9    in make_tsig (classes', classrel', default, tycons, log_types, univ_witness, abbrs, arities) end;
    1.10  
    1.11  
    1.12 @@ -540,10 +540,11 @@
    1.13  fun ext_tsig_classrel tsig pairs =
    1.14    let
    1.15      val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
    1.16 +    val cert = cert_class tsig;
    1.17  
    1.18      (* FIXME clean! *)
    1.19      val classrel' =
    1.20 -      merge_classrel (classrel, Symtab.make (map (fn (c1, c2) => (c1, [c2])) pairs));
    1.21 +      merge_classrel (classrel, Symtab.make (map (fn (c1, c2) => (cert c1, [cert c2])) pairs));
    1.22    in
    1.23      make_tsig (classes, classrel', default, tycons, log_types, univ_witness, abbrs, arities)
    1.24      |> rebuild_tsig