| author | wenzelm |
| Wed, 13 Nov 1996 10:59:53 +0100 | |
| changeset 2184 | 99805d7652a9 |
| parent 2183 | 8d42a7bccf0b |
| child 2185 | f9686e7e6d4d |
| src/Pure/sign.ML | file | annotate | diff | comparison | revisions |
--- 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);