# HG changeset patch
# User wenzelm
# Date 847879193 -3600
# Node ID 99805d7652a90d5c118df6561fd58dda2be94ef2
# Parent  8d42a7bccf0b0880dff8e46c71c4811be8b2e7ec
tuned subsig;

diff -r 8d42a7bccf0b -r 99805d7652a9 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Nov 13 10:47:08 1996 +0100
+++ b/src/Pure/sign.ML	Wed Nov 13 10:59:53 1996 +0100
@@ -103,7 +103,8 @@
 fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
   | is_draft _ = false;
 
-fun subsig (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = subset_stamp(s1,s2);
+fun subsig (Sg{stamps=s1,...}, Sg{stamps=s2,...}) =
+  s1 = s2 orelse subset_stamp (s1, s2);
 
 fun eq_sg (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = eq_set_stamp(s1,s2);