Merge mixins of distinct interpretations with same base.

--- a/src/Pure/Isar/locale.ML	Wed May 26 18:19:36 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Wed May 26 21:20:18 2010 +0200
@@ -170,6 +170,31 @@
 fun dependencies_of thy name = the_locale thy name |>
   #dependencies |> map fst;
 
+(* Print instance and qualifiers *)
+
+fun pretty_reg thy (name, morph) =
+  let
+    val name' = extern thy name;
+    val ctxt = ProofContext.init_global thy;
+    fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
+    fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
+    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
+    fun prt_term' t = if !show_types
+      then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
+        Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
+      else prt_term t;
+    fun prt_inst ts =
+      Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
+
+    val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
+    val ts = instance_of thy name morph;
+  in
+    case qs of
+       [] => prt_inst ts
+     | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
+         Pretty.brk 1, prt_inst ts]
+  end;
+
 
 (*** Activate context elements of locale ***)
 
@@ -348,9 +373,23 @@
        entries for empty lists may be omitted *)
   val empty = (Idtab.empty, Inttab.empty);
   val extend = I;
-  fun merge ((r1, m1), (r2, m2)) : T =
-    (Idtab.join (K (fst)) (r1, r2), (* pick left registration, FIXME? *)
-      Inttab.join (K (Library.merge (eq_snd op =))) (m1, m2));
+  fun merge ((reg1, mix1), (reg2, mix2)) : T =
+    (Idtab.join (fn id => fn (r1 as (_, s1), r2 as (_, s2)) =>
+        if s1 = s2 then raise Idtab.SAME else raise Idtab.DUP id) (reg1, reg2),
+      Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2))
+    handle Idtab.DUP id =>
+      (* distinct interpretations with same base: merge their mixins *)
+      let
+        val (_, s1) = Idtab.lookup reg1 id |> the;
+        val (morph2, s2) = Idtab.lookup reg2 id |> the;
+        val reg2' = Idtab.update (id, (morph2, s1)) reg2;
+        val mix2' = case Inttab.lookup mix2 s2 of
+              NONE => mix2 |
+              SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs);
+        val _ = warning "Removed duplicate interpretation after retrieving its mixins.";
+        (* FIXME print interpretations,
+           which is not straightforward without theory context *)
+      in merge ((reg1, mix1), (reg2', mix2')) end;
     (* FIXME consolidate with dependencies, consider one data slot only *)
 );
 
@@ -421,29 +460,6 @@
 
 (* Diagnostic *)
 
-fun pretty_reg thy (name, morph) =
-  let
-    val name' = extern thy name;
-    val ctxt = ProofContext.init_global thy;
-    fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
-    fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
-    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
-    fun prt_term' t = if !show_types
-      then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
-        Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
-      else prt_term t;
-    fun prt_inst ts =
-      Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
-
-    val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
-    val ts = instance_of thy name morph;
-  in
-    case qs of
-       [] => prt_inst ts
-     | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
-         Pretty.brk 1, prt_inst ts]
-  end;
-
 fun print_registrations thy raw_name =
   (case these_registrations thy (intern thy raw_name) of
       [] => Pretty.str ("no interpretations")