# HG changeset patch # User wenzelm # Date 879519069 -3600 # Node ID 22e3f0368c85eef4151332737bcd170deee469d6 # Parent a5c947d7c56cc178fa9f637a144402a60bbedf31 merge_refs: check for different versions of theories; diff -r a5c947d7c56c -r 22e3f0368c85 src/Pure/sign.ML --- a/src/Pure/sign.ML Thu Nov 13 17:55:27 1997 +0100 +++ b/src/Pure/sign.ML Fri Nov 14 15:51:09 1997 +0100 @@ -848,15 +848,27 @@ (** merge signatures **) (*exception TERM*) +(* merge_stamps *) + +fun merge_stamps stamps1 stamps2 = + let val stamps = merge_rev_lists stamps1 stamps2 in + (case duplicates (map ! stamps) of + [] => stamps + | dups => raise TERM ("Attempt to merge different versions of theories " + ^ commas_quote dups, [])) + end; + + (* merge of sg_refs -- trivial only *) -fun merge_refs (sgr1 as SgRef (Some (ref sg1)), - sgr2 as SgRef (Some (ref sg2))) = +fun merge_refs (sgr1 as SgRef (Some (ref (sg1 as Sg ({stamps = s1, ...}, _)))), + sgr2 as SgRef (Some (ref (sg2 as Sg ({stamps = s2, ...}, _))))) = if fast_subsig (sg2, sg1) then sgr1 else if fast_subsig (sg1, sg2) then sgr2 else if subsig (sg2, sg1) then sgr1 else if subsig (sg1, sg2) then sgr2 - else raise TERM ("Attempt to do non-trivial merge of signatures", []) + else (merge_stamps s1 s2; (*check for different versions*) + raise TERM ("Attempt to do non-trivial merge of signatures", [])) | merge_refs _ = sys_error "Sign.merge_refs"; @@ -878,13 +890,8 @@ val id = ref ""; val self_ref = ref sg1; (*dummy value*) val self = SgRef (Some self_ref); - val stamps = merge_rev_lists stamps1 stamps2; - val _ = - (case duplicates (map ! stamps) of - [] => () - | dups => raise TERM ("Attempt to merge different versions of theories " - ^ commas_quote dups, [])); + val stamps = merge_stamps stamps1 stamps2; val tsig = Type.merge_tsigs (tsig1, tsig2); val const_tab = Symtab.merge (op =) (const_tab1, const_tab2) handle Symtab.DUPS cs =>