# HG changeset patch
# User wenzelm
# Date 1269631803 -3600
# Node ID 6343ebe9715db5c14b3c1cc42d1a019ff95b4d7c
# Parent  30d42bfd01748495653882bca88e335bd1eef9c8# Parent  ea3d4691a8c6e50192ac88236d68147c04bcd676
merged

diff -r 30d42bfd0174 -r 6343ebe9715d src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Fri Mar 26 18:03:01 2010 +0100
+++ b/src/Pure/General/graph.ML	Fri Mar 26 20:30:03 2010 +0100
@@ -202,13 +202,17 @@
 
 fun no_edges (i, _) = (i, ([], []));
 
-fun join f (Graph tab1, G2 as Graph tab2) =
-  let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1)
-  in fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2))) end;
+fun join f (G1 as Graph tab1, G2 as Graph tab2) =
+  let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in
+    if pointer_eq (G1, G2) then G1
+    else fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map no_edges tab2)))
+  end;
 
-fun gen_merge add eq (Graph tab1, G2 as Graph tab2) =
-  let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2)
-  in fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2))) end;
+fun gen_merge add eq (G1 as Graph tab1, G2 as Graph tab2) =
+  let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2) in
+    if pointer_eq (G1, G2) then G1
+    else fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map no_edges tab2)))
+  end;
 
 fun merge eq GG = gen_merge add_edge eq GG;
 
@@ -273,9 +277,11 @@
   |> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]);
 
 fun merge_trans_acyclic eq (G1, G2) =
-  merge_acyclic eq (G1, G2)
-  |> fold add_edge_trans_acyclic (diff_edges G1 G2)
-  |> fold add_edge_trans_acyclic (diff_edges G2 G1);
+  if pointer_eq (G1, G2) then G1
+  else
+    merge_acyclic eq (G1, G2)
+    |> fold add_edge_trans_acyclic (diff_edges G1 G2)
+    |> fold add_edge_trans_acyclic (diff_edges G2 G1);
 
 
 (*final declarations of this structure!*)
diff -r 30d42bfd0174 -r 6343ebe9715d src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Mar 26 18:03:01 2010 +0100
+++ b/src/Pure/library.ML	Fri Mar 26 20:30:03 2010 +0100
@@ -774,6 +774,8 @@
             | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
   in match (space_explode "*" pat) str end;
 
+
+
 (** lists as sets -- see also Pure/General/ord_list.ML **)
 
 (* canonical operations *)
diff -r 30d42bfd0174 -r 6343ebe9715d src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Fri Mar 26 18:03:01 2010 +0100
+++ b/src/Pure/sorts.ML	Fri Mar 26 20:30:03 2010 +0100
@@ -254,18 +254,21 @@
           (filter_out (fn (c'', (_, Ss'')) => c = c'' andalso Ss'' = Ss') ars)
       else err_conflict pp t NONE (c, Ss) (c, Ss'));
 
-fun insert_ars pp algebra (t, ars) arities =
+in
+
+fun insert_ars pp algebra t = fold_rev (insert pp algebra t);
+
+fun insert_complete_ars pp algebra (t, ars) arities =
   let val ars' =
     Symtab.lookup_list arities t
-    |> fold_rev (fold_rev (insert pp algebra t)) (map (complete algebra) ars)
+    |> fold_rev (insert_ars pp algebra t) (map (complete algebra) ars);
   in Symtab.update (t, ars') arities end;
 
-in
-
-fun add_arities pp arg algebra = algebra |> map_arities (insert_ars pp algebra arg);
+fun add_arities pp arg algebra =
+  algebra |> map_arities (insert_complete_ars pp algebra arg);
 
 fun add_arities_table pp algebra =
-  Symtab.fold (fn (t, ars) => insert_ars pp algebra (t, map snd ars));
+  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, map snd ars));
 
 end;
 
@@ -291,11 +294,22 @@
   let
     val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
       handle Graph.DUP c => err_dup_class c
-          | Graph.CYCLES css => err_cyclic_classes pp css;
+        | Graph.CYCLES css => err_cyclic_classes pp css;
     val algebra0 = make_algebra (classes', Symtab.empty);
-    val arities' = Symtab.empty
-      |> add_arities_table pp algebra0 arities1
-      |> add_arities_table pp algebra0 arities2;
+    val arities' =
+      (case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of
+        (true, true) => arities1
+      | (true, false) =>  (*no completion*)
+          (arities1, arities2) |> Symtab.join (fn t => fn (ars1, ars2) =>
+            if pointer_eq (ars1, ars2) then raise Symtab.SAME
+            else insert_ars pp algebra0 t ars2 ars1)
+      | (false, true) =>  (*unary completion*)
+          Symtab.empty
+          |> add_arities_table pp algebra0 arities1
+      | (false, false) => (*binary completion*)
+          Symtab.empty
+          |> add_arities_table pp algebra0 arities1
+          |> add_arities_table pp algebra0 arities2);
   in make_algebra (classes', arities') end;