# HG changeset patch
# User wenzelm
# Date 981056754 -3600
# Node ID 72a76580ed2fa3b5ddd605cb8276470e584b264c
# Parent  41de937d338b5c818c92aa40b1ab509776e6fd20
ext_classrel: certify_class;

diff -r 41de937d338b -r 72a76580ed2f src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Feb 01 20:45:11 2001 +0100
+++ b/src/Pure/type.ML	Thu Feb 01 20:45:54 2001 +0100
@@ -531,7 +531,7 @@
 fun ext_tsig_classes tsig new_classes =
   let
     val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
-    val (classes',classrel') = extend_classes (classes,classrel,new_classes);
+    val (classes', classrel') = extend_classes (classes,classrel, new_classes);
   in make_tsig (classes', classrel', default, tycons, log_types, univ_witness, abbrs, arities) end;
 
 
@@ -540,10 +540,11 @@
 fun ext_tsig_classrel tsig pairs =
   let
     val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
+    val cert = cert_class tsig;
 
     (* FIXME clean! *)
     val classrel' =
-      merge_classrel (classrel, Symtab.make (map (fn (c1, c2) => (c1, [c2])) pairs));
+      merge_classrel (classrel, Symtab.make (map (fn (c1, c2) => (cert c1, [cert c2])) pairs));
   in
     make_tsig (classes, classrel', default, tycons, log_types, univ_witness, abbrs, arities)
     |> rebuild_tsig