src/Pure/sign.ML
changeset 4228 22e3f0368c85
parent 4227 a5c947d7c56c
child 4249 34b7aafdc1bc
     1.1 --- a/src/Pure/sign.ML	Thu Nov 13 17:55:27 1997 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Nov 14 15:51:09 1997 +0100
     1.3 @@ -848,15 +848,27 @@
     1.4  
     1.5  (** merge signatures **)    	(*exception TERM*)
     1.6  
     1.7 +(* merge_stamps *)
     1.8 +
     1.9 +fun merge_stamps stamps1 stamps2 =
    1.10 +  let val stamps = merge_rev_lists stamps1 stamps2 in
    1.11 +    (case duplicates (map ! stamps) of
    1.12 +      [] => stamps
    1.13 +    | dups => raise TERM ("Attempt to merge different versions of theories "
    1.14 +        ^ commas_quote dups, []))
    1.15 +  end;
    1.16 +
    1.17 +
    1.18  (* merge of sg_refs -- trivial only *)
    1.19  
    1.20 -fun merge_refs (sgr1 as SgRef (Some (ref sg1)),
    1.21 -        sgr2 as SgRef (Some (ref sg2))) =
    1.22 +fun merge_refs (sgr1 as SgRef (Some (ref (sg1 as Sg ({stamps = s1, ...}, _)))),
    1.23 +        sgr2 as SgRef (Some (ref (sg2 as Sg ({stamps = s2, ...}, _))))) =
    1.24        if fast_subsig (sg2, sg1) then sgr1
    1.25        else if fast_subsig (sg1, sg2) then sgr2
    1.26        else if subsig (sg2, sg1) then sgr1
    1.27        else if subsig (sg1, sg2) then sgr2
    1.28 -      else raise TERM ("Attempt to do non-trivial merge of signatures", [])
    1.29 +      else (merge_stamps s1 s2; (*check for different versions*)
    1.30 +        raise TERM ("Attempt to do non-trivial merge of signatures", []))
    1.31    | merge_refs _ = sys_error "Sign.merge_refs";
    1.32  
    1.33  
    1.34 @@ -878,13 +890,8 @@
    1.35        val id = ref "";
    1.36        val self_ref = ref sg1;                   (*dummy value*)
    1.37        val self = SgRef (Some self_ref);
    1.38 -      val stamps = merge_rev_lists stamps1 stamps2;
    1.39 -      val _ =
    1.40 -        (case duplicates (map ! stamps) of
    1.41 -          [] => ()
    1.42 -        | dups => raise TERM ("Attempt to merge different versions of theories "
    1.43 -            ^ commas_quote dups, []));
    1.44  
    1.45 +      val stamps = merge_stamps stamps1 stamps2;
    1.46        val tsig = Type.merge_tsigs (tsig1, tsig2);
    1.47        val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
    1.48          handle Symtab.DUPS cs =>