src/Pure/Isar/locale.ML

 
 (*** Registrations: interpretations in theories ***)
 
 structure Registrations = Theory_Data
 (
-  type T = ((string * (morphism * morphism)) * serial) list *
+  type T = (((string * term list) * (morphism * morphism)) * serial) list *
     (* registrations, in reverse order of declaration;
        serial points to mixin list *)
     (serial * ((morphism * bool) * serial) list) list;
     (* alist of mixin lists, per list mixins in reverse order of declaration;
        lists indexed by registration serial,

 );
 
 
 (* Primitive operations *)
 
-fun add_reg export (dep, morph) =
-  Registrations.map (apfst (cons ((dep, (morph, export)), serial ())));
+fun add_reg thy export (name, morph) =
+  Registrations.map (apfst (cons (((name, instance_of thy name (morph $> export)), (morph, export)), serial ())));
 
 fun add_mixin serial' mixin =
   (* registration to be amended identified by its serial id *)
   Registrations.map (apsnd (AList.map_default (op =) (serial', []) (cons (mixin, serial ()))));
 
 fun get_mixins thy (name, morph) =
   let
     val (regs, mixins) = Registrations.get thy;
   in
-    case find_first (fn ((name', (morph', export')), _) => ident_eq
-      ((name', instance_of thy name' (morph' $> export')), (name, instance_of thy name morph))) (rev regs) of
+    case find_first (fn (((name', inst'), (morph', export')), _) => ident_eq
+      ((name', inst'), (name, instance_of thy name morph))) (rev regs) of
       NONE => []
     | SOME (_, serial) => the_default [] (AList.lookup (op =) mixins serial)
   end;
 
 fun collect_mixins thy (name, morph) =

 fun reg_morph mixins ((name, (base, export)), serial) =
   let val mix = the_default [] (AList.lookup (op =) mixins serial) |> compose_mixins;
   in (name, base $> mix $> export) end;
 
 fun these_registrations thy name = Registrations.get thy
-  |>> filter (curry (op =) name o fst o fst)
+  |>> filter (curry (op =) name o fst o fst o fst)
   (* with inherited mixins *)
-  |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
+  |-> (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 (* FIXME clone *)
   (* with inherited mixins *)
-  |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
+  |-> (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
     val {notes, ...} = the_locale thy name;

 
 fun amend_registration (name, morph) mixin export thy =
   let
     val regs = Registrations.get thy |> fst;
     val base = instance_of thy name (morph $> export);
-    fun match ((name', (morph', export')), _) =
-      ident_eq ((name, base), (name', instance_of thy name' (morph' $> export)));
+    fun match (((name', inst'), _), _) = ident_eq ((name, base), (name', inst'));
   in
     case find_first match (rev regs) of
         NONE => error ("No interpretation of locale " ^
           quote (extern thy name) ^ " and\nparameter instantiation " ^
           space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^

     if member (ident_le thy) (get_idents (Context.Theory thy)) (name, inst)
     then thy
     else
       (get_idents (Context.Theory thy), thy)
       (* add new registrations with inherited mixins *)
-      |> roundup thy (add_reg export) export (name, morph)
+      |> roundup thy (add_reg thy export) export (name, morph)
       |> snd
       (* add mixin *)
       |> (case mixin of NONE => I
            | SOME mixin => amend_registration (name, morph) mixin export)
       (* activate import hierarchy as far as not already active *)