Sign.merge vs. Sign.nontriv_merge;
authorwenzelm
Thu Feb 12 17:43:53 1998 +0100 (1998-02-12)
changeset 4627ae95666c71cc
parent 4626 51dd12f34c78
child 4628 0c7e97836e3c
Sign.merge vs. Sign.nontriv_merge;
src/Pure/sign.ML
src/Pure/theory.ML
     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, []));
     2.1 --- a/src/Pure/theory.ML	Thu Feb 12 16:54:01 1998 +0100
     2.2 +++ b/src/Pure/theory.ML	Thu Feb 12 17:43:53 1998 +0100
     2.3 @@ -385,7 +385,7 @@
     2.4  (** merge theories **)		(*exception ERROR*)
     2.5  
     2.6  fun merge_sign (sg, thy) =
     2.7 -  Sign.merge (sg, sign_of thy) handle TERM (msg, _) => error msg;
     2.8 +  Sign.nontriv_merge (sg, sign_of thy) handle TERM (msg, _) => error msg;
     2.9  
    2.10  (*merge list of theories from left to right, preparing extend*)
    2.11  fun prep_ext_merge thys =