# 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);