# HG changeset patch
# User wenzelm
# Date 771761040 -7200
# Node ID 95e1d4faa86323b91268bd43cc166fdf99b064d2
# Parent  1e0f1973536d6febac38c7df21de4539c37bebeb
added add_classrel;

diff -r 1e0f1973536d -r 95e1d4faa863 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Jun 09 11:11:03 1994 +0200
+++ b/src/Pure/sign.ML	Thu Jun 16 12:04:00 1994 +0200
@@ -40,6 +40,7 @@
     val certify_term: sg -> term -> term * typ * int
     val read_typ: sg * (indexname -> sort option) -> string -> typ
     val add_classes: (class list * class * class list) list -> sg -> sg
+    val add_classrel: (class * class) list -> sg -> sg
     val add_defsort: sort -> sg -> sg
     val add_types: (string * int * mixfix) list -> sg -> sg
     val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
@@ -78,7 +79,7 @@
 structure BasicSyntax: BASIC_SYNTAX = Syntax;
 structure Pretty = Syntax.Pretty;
 structure Type = Type;
-open BasicSyntax Type;
+open BasicSyntax (* FIXME *) Type;
 open Syntax.Mixfix;   (* FIXME *)
 
 
@@ -266,9 +267,6 @@
   else
     extend_tsig tsig (map (fn (_, c, cs) => (c, cs)) classes, [], [], []);
 
-fun ext_tsig_defsort tsig defsort =
-  extend_tsig tsig ([], defsort, [], []);
-
 fun ext_tsig_types tsig types =
   extend_tsig tsig ([], [], map (fn (t, n) => ([t], n)) types, []);
 
@@ -414,6 +412,12 @@
   end;
 
 
+(* add to subclass relation *)
+
+fun ext_classrel (syn, tsig, ctab) pairs =
+  (syn, ext_tsig_subclass tsig pairs, ctab);
+
+
 (* add syntactic translations *)
 
 fun ext_trfuns (syn, tsig, ctab) trfuns =
@@ -445,6 +449,7 @@
 (* the external interfaces *)
 
 val add_classes   = extend_sign ext_classes "#";
+val add_classrel  = extend_sign ext_classrel "#";
 val add_defsort   = extend_sign ext_defsort "#";
 val add_types     = extend_sign ext_types "#";
 val add_tyabbrs   = extend_sign ext_tyabbrs "#";
diff -r 1e0f1973536d -r 95e1d4faa863 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Jun 09 11:11:03 1994 +0200
+++ b/src/Pure/thm.ML	Thu Jun 16 12:04:00 1994 +0200
@@ -35,6 +35,7 @@
   (* FIXME *)
   local open Sign.Syntax Sign.Syntax.Mixfix in  (* FIXME remove ...Mixfix *)
     val add_classes: (class list * class * class list) list -> theory -> theory
+    val add_classrel: (class * class) list -> theory -> theory
     val add_defsort: sort -> theory -> theory
     val add_types: (string * int * mixfix) list -> theory -> theory
     val add_tyabbrs: (string * string list * string * mixfix) list
@@ -117,7 +118,7 @@
          bool*bool -> meta_simpset -> (meta_simpset -> thm -> thm option)
            -> cterm -> thm
   val set_mk_rews: meta_simpset * (thm -> thm list) -> meta_simpset
-  val rep_theory: theory -> {sign: Sign.sg, new_axioms: term Sign.Symtab.table, 
+  val rep_theory: theory -> {sign: Sign.sg, new_axioms: term Sign.Symtab.table,
     parents: theory list}
   val subthy: theory * theory -> bool
   val eq_thy: theory * theory -> bool
@@ -336,6 +337,7 @@
   ext_thy thy (extfun decls sign) [];
 
 val add_classes   = ext_sg Sign.add_classes;
+val add_classrel  = ext_sg Sign.add_classrel;
 val add_defsort   = ext_sg Sign.add_defsort;
 val add_types     = ext_sg Sign.add_types;
 val add_tyabbrs   = ext_sg Sign.add_tyabbrs;