--- a/src/Pure/sign.ML Wed Dec 29 10:14:58 1993 +0100
+++ b/src/Pure/sign.ML Thu Dec 30 10:18:23 1993 +0100
@@ -46,6 +46,7 @@
val pprint_ctyp: ctyp -> pprint_args -> unit
val string_of_term: sg -> term -> string
val string_of_typ: sg -> typ -> string
+ val subsig: sg * sg -> bool
val pprint_term: sg -> term -> pprint_args -> unit
val pprint_typ: sg -> typ -> pprint_args -> unit
val term_of: cterm -> term
@@ -74,6 +75,8 @@
fun rep_sg (Sg args) = args;
+fun subsig(Sg{stamps=s1,...},Sg{stamps=s2,...}) = s1 subset s2;
+
fun string_of_typ(Sg{tsig,syn,...}) = Syntax.string_of_typ syn;
fun pprint_typ(Sg{syn,...}) = Pretty.pprint o Pretty.quote o (Syntax.pretty_typ syn);