src/Pure/Isar/locale.ML

--- a/src/Pure/Isar/locale.ML	Thu May 13 13:29:43 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Thu May 13 13:30:16 2010 +0200
@@ -384,9 +384,10 @@
   |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
     (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
 
-fun all_registrations thy = Registrations.get thy
-  |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
-  (* without inherited mixins *)
+fun all_registrations thy = Registrations.get thy (* FIXME clone *)
+  (* with inherited mixins *)
+  |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
+    (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
 
 fun activate_notes' activ_elem transfer thy export (name, morph) input =
   let
@@ -462,19 +463,21 @@
 fun add_registration (name, base_morph) mixin export thy =
   let
     val base = instance_of thy name base_morph;
+    val mix = case mixin of NONE => Morphism.identity
+          | SOME (mix, _) => mix;
   in
     if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
     then thy
     else
       (get_idents (Context.Theory thy), thy)
       (* add new registrations with inherited mixins *)
-      |> roundup thy (add_reg export) export (name, base_morph)
+      |> roundup thy (add_reg export) export (name, base_morph $> mix) (* FIXME *)
       |> snd
       (* add mixin *)
       |> (case mixin of NONE => I
-           | SOME mixin => amend_registration (name, base_morph) mixin export)
+           | SOME mixin => amend_registration (name, base_morph $> mix) mixin export)
       (* activate import hierarchy as far as not already active *)
-      |> Context.theory_map (activate_facts' export (name, base_morph))
+      |> Context.theory_map (activate_facts' export (name, base_morph $> mix))
   end;