src/Pure/sign.ML
changeset 2184 99805d7652a9
parent 2180 934572a94139
child 2185 f9686e7e6d4d
     1.1 --- a/src/Pure/sign.ML	Wed Nov 13 10:47:08 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Nov 13 10:59:53 1996 +0100
     1.3 @@ -103,7 +103,8 @@
     1.4  fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
     1.5    | is_draft _ = false;
     1.6  
     1.7 -fun subsig (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = subset_stamp(s1,s2);
     1.8 +fun subsig (Sg{stamps=s1,...}, Sg{stamps=s2,...}) =
     1.9 +  s1 = s2 orelse subset_stamp (s1, s2);
    1.10  
    1.11  fun eq_sg (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = eq_set_stamp(s1,s2);
    1.12