src/Pure/sign.ML
changeset 2180 934572a94139
parent 2144 ddb8499c772b
child 2184 99805d7652a9
     1.1 --- a/src/Pure/sign.ML	Tue Nov 12 13:20:36 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Nov 13 10:38:08 1996 +0100
     1.3 @@ -88,20 +88,30 @@
     1.4  val tsig_of = #tsig o rep_sg;
     1.5  
     1.6  
     1.7 -(* stamps *)
     1.8 +(*** Stamps ***)
     1.9 +
    1.10 +(*Avoiding polymorphic equality: 10* speedup*)
    1.11 +fun mem_stamp (_:string ref, []) = false
    1.12 +  | mem_stamp (x, y::xs) = x=y orelse mem_stamp(x,xs);
    1.13 +
    1.14 +fun subset_stamp ([], ys) = true
    1.15 +  | subset_stamp (x :: xs, ys) = mem_stamp(x, ys) andalso subset_stamp(xs, ys);
    1.16 +
    1.17 +fun eq_set_stamp (xs, ys) =
    1.18 +    xs = ys orelse (subset_stamp (xs, ys) andalso subset_stamp (ys, xs));
    1.19  
    1.20  fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
    1.21    | is_draft _ = false;
    1.22  
    1.23 -fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = s1 subset s2;
    1.24 +fun subsig (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = subset_stamp(s1,s2);
    1.25  
    1.26 -fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
    1.27 +fun eq_sg (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = eq_set_stamp(s1,s2);
    1.28  
    1.29  (* test if same theory names are contained in signatures' stamps,
    1.30     i.e. if signatures belong to same theory but not necessarily to the same
    1.31     version of it*)
    1.32  fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
    1.33 -  eq_set (pairself (map (op !)) (s1, s2));
    1.34 +  eq_set_string (pairself (map (op !)) (s1, s2));
    1.35  
    1.36  
    1.37  (* consts *)