src/Pure/sign.ML
changeset 4627 ae95666c71cc
parent 4619 72edc2a9200f
child 4844 4fb63c77f2df
     1.1 --- a/src/Pure/sign.ML	Thu Feb 12 16:54:01 1998 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Feb 12 17:43:53 1998 +0100
     1.3 @@ -124,8 +124,9 @@
     1.4    val put_data: string * object -> sg -> sg
     1.5    val print_data: sg -> string -> unit
     1.6    val merge_refs: sg_ref * sg_ref -> sg_ref
     1.7 +  val merge: sg * sg -> sg
     1.8    val prep_ext: sg -> sg
     1.9 -  val merge: sg * sg -> sg
    1.10 +  val nontriv_merge: sg * sg -> sg
    1.11    val pre_pure: sg
    1.12    val const_of_class: class -> string
    1.13    val class_of_const: string -> class
    1.14 @@ -889,7 +890,7 @@
    1.15    end;
    1.16  
    1.17  
    1.18 -(* merge of sg_refs -- trivial only *)
    1.19 +(* implicit merge -- trivial only *)
    1.20  
    1.21  fun merge_refs (sgr1 as SgRef (Some (ref (sg1 as Sg ({stamps = s1, ...}, _)))),
    1.22          sgr2 as SgRef (Some (ref (sg2 as Sg ({stamps = s2, ...}, _))))) =
    1.23 @@ -901,6 +902,8 @@
    1.24          raise TERM ("Attempt to do non-trivial merge of signatures", []))
    1.25    | merge_refs _ = sys_error "Sign.merge_refs";
    1.26  
    1.27 +val merge = deref o merge_refs o pairself self_ref;
    1.28 +
    1.29  
    1.30  (* proper merge *)
    1.31  
    1.32 @@ -942,7 +945,7 @@
    1.33        self_ref := sign; sign
    1.34      end;
    1.35  
    1.36 -fun merge sg1_sg2 =
    1.37 +fun nontriv_merge sg1_sg2 =
    1.38    (case handle_error merge_aux sg1_sg2 of
    1.39      OK sg => sg
    1.40    | Error msg => raise TERM (msg, []));