# HG changeset patch
# User wenzelm
# Date 887301833 -3600
# Node ID ae95666c71cc075046b98c528de9df31dbcaad85
# Parent  51dd12f34c784528a053db13e9d384d7cec102c2
Sign.merge vs. Sign.nontriv_merge;

diff -r 51dd12f34c78 -r ae95666c71cc src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Feb 12 16:54:01 1998 +0100
+++ b/src/Pure/sign.ML	Thu Feb 12 17:43:53 1998 +0100
@@ -124,8 +124,9 @@
   val put_data: string * object -> sg -> sg
   val print_data: sg -> string -> unit
   val merge_refs: sg_ref * sg_ref -> sg_ref
+  val merge: sg * sg -> sg
   val prep_ext: sg -> sg
-  val merge: sg * sg -> sg
+  val nontriv_merge: sg * sg -> sg
   val pre_pure: sg
   val const_of_class: class -> string
   val class_of_const: string -> class
@@ -889,7 +890,7 @@
   end;
 
 
-(* merge of sg_refs -- trivial only *)
+(* implicit merge -- trivial only *)
 
 fun merge_refs (sgr1 as SgRef (Some (ref (sg1 as Sg ({stamps = s1, ...}, _)))),
         sgr2 as SgRef (Some (ref (sg2 as Sg ({stamps = s2, ...}, _))))) =
@@ -901,6 +902,8 @@
         raise TERM ("Attempt to do non-trivial merge of signatures", []))
   | merge_refs _ = sys_error "Sign.merge_refs";
 
+val merge = deref o merge_refs o pairself self_ref;
+
 
 (* proper merge *)
 
@@ -942,7 +945,7 @@
       self_ref := sign; sign
     end;
 
-fun merge sg1_sg2 =
+fun nontriv_merge sg1_sg2 =
   (case handle_error merge_aux sg1_sg2 of
     OK sg => sg
   | Error msg => raise TERM (msg, []));
diff -r 51dd12f34c78 -r ae95666c71cc src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Feb 12 16:54:01 1998 +0100
+++ b/src/Pure/theory.ML	Thu Feb 12 17:43:53 1998 +0100
@@ -385,7 +385,7 @@
 (** merge theories **)		(*exception ERROR*)
 
 fun merge_sign (sg, thy) =
-  Sign.merge (sg, sign_of thy) handle TERM (msg, _) => error msg;
+  Sign.nontriv_merge (sg, sign_of thy) handle TERM (msg, _) => error msg;
 
 (*merge list of theories from left to right, preparing extend*)
 fun prep_ext_merge thys =