src/Pure/sign.ML
changeset 1241 bfc93c86f0a1
parent 1239 2c0d94151e74
child 1393 73b6b003c6ca
     1.1 --- a/src/Pure/sign.ML	Fri Sep 01 13:16:24 1995 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Sep 01 13:27:48 1995 +0200
     1.3 @@ -20,6 +20,7 @@
     1.4         stamps: string ref list}
     1.5      val subsig: sg * sg -> bool
     1.6      val eq_sg: sg * sg -> bool
     1.7 +    val same_sg: sg * sg -> bool
     1.8      val is_draft: sg -> bool
     1.9      val const_type: sg -> string -> typ option
    1.10      val classes: sg -> class list
    1.11 @@ -107,6 +108,12 @@
    1.12  
    1.13  fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
    1.14  
    1.15 +(* test if same theory names are contained in signatures' stamps,
    1.16 +   i.e. if signatures belong to same theory but not necessarily to the same
    1.17 +   version of it*)
    1.18 +fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
    1.19 +  eq_set (pairself (map (op !)) (s1, s2));
    1.20 +
    1.21  
    1.22  (* consts *)
    1.23