src/Pure/Isar/locale.ML

   val intro_add: attribute
   val unfold_add: attribute
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Registrations and dependencies *)
-  val add_registration: string * morphism -> (morphism * bool) option ->
-    morphism -> Context.generic -> Context.generic
-  val activate_fragment: string * morphism -> (morphism * bool) option -> morphism ->
-    local_theory -> local_theory
-  val activate_fragment_nonbrittle: string * morphism -> (morphism * bool) option -> morphism ->
-    local_theory -> local_theory
-  val amend_registration: string * morphism -> morphism * bool ->
-    morphism -> Context.generic -> Context.generic
+  type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism}
+  val amend_registration: registration -> Context.generic -> Context.generic
+  val add_registration: registration -> Context.generic -> Context.generic
+  val activate_fragment: registration -> local_theory -> local_theory
+  val activate_fragment_nonbrittle: registration -> local_theory -> local_theory
   val registrations_of: Context.generic -> string -> (string * morphism) list
-  val add_dependency: string -> string * morphism -> (morphism * bool) option ->
-    morphism -> theory -> theory
+  val add_dependency: string -> registration -> theory -> theory
 
   (* Diagnostic *)
   val hyp_spec_of: theory -> string -> Element.context_i list
   val print_locales: bool -> theory -> unit
   val print_locale: theory -> bool -> xstring * Position.T -> unit

   end;
 
 
 (*** Add and extend registrations ***)
 
-fun amend_registration (name, morph) mixin export context =
-  let
-    val thy = Context.theory_of context;
-    val ctxt = Context.proof_of context;
-
-    val regs = Registrations.get context |> fst;
-    val base = instance_of thy name (morph $> export);
-    val serial' =
-      (case Idtab.lookup regs (name, base) of
-        NONE =>
-          error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^
-            " with\nparameter instantiation " ^
-            space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
-            " available")
-      | SOME (_, serial') => serial');
-  in
-    add_mixin serial' mixin context
-  end;
+type registration = Locale.registration;
+
+fun amend_registration {mixin = NONE, ...} context = context
+  | amend_registration {dep = (name, morph), mixin = SOME mixin, export} context =
+      let
+        val thy = Context.theory_of context;
+        val ctxt = Context.proof_of context;
+
+        val regs = Registrations.get context |> fst;
+        val base = instance_of thy name (morph $> export);
+        val serial' =
+          (case Idtab.lookup regs (name, base) of
+            NONE =>
+              error ("No interpretation of locale " ^ quote (markup_name ctxt name) ^
+                " with\nparameter instantiation " ^
+                space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
+                " available")
+          | SOME (_, serial') => serial');
+      in
+        add_mixin serial' mixin context
+      end;
 
 (* Note that a registration that would be subsumed by an existing one will not be
    generated, and it will not be possible to amend it. *)
 
-fun add_registration (name, base_morph) mixin export context =
+fun add_registration {dep = (name, base_morph), mixin, export} context =
   let
     val thy = Context.theory_of context;
     val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
     val morph = base_morph $> mix;
     val inst = instance_of thy name morph;

       (idents, context)
       (* add new registrations with inherited mixins *)
       |> 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)
+      |> amend_registration {dep = (name, morph), mixin = mixin, export = export}
       (* activate import hierarchy as far as not already active *)
       |> activate_facts (SOME export) (name, morph)
   end;
 
 
 (* locale fragments within local theory *)
 
-fun activate_fragment_nonbrittle dep_morph mixin export lthy =
+fun activate_fragment_nonbrittle registration lthy =
   let val n = Local_Theory.level lthy in
     lthy |> Local_Theory.map_contexts (fn level =>
-      level = n - 1 ? Context.proof_map (add_registration dep_morph mixin export))
-  end;
-
-fun activate_fragment dep_morph mixin export =
-  Local_Theory.mark_brittle #> activate_fragment_nonbrittle dep_morph mixin export;
+      level = n - 1 ? Context.proof_map (add_registration registration))
+  end;
+
+fun activate_fragment registration =
+  Local_Theory.mark_brittle #> activate_fragment_nonbrittle registration;
 
 
 
 (*** Dependencies ***)
 

           " not a sublocale of " ^ quote (extern thy loc))
       | SOME (_, serial') => change_locale ...
   end;
 *)
 
-fun add_dependency loc (name, morph) mixin export thy =
+fun add_dependency loc {dep = (name, morph), mixin, export} thy =
   let
     val serial' = serial ();
     val thy' = thy |>
       (change_locale loc o apsnd)
         (apfst (cons ((name, (morph, export)), serial')) #>
           apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin));
     val context' = Context.Theory thy';
     val (_, regs) =
       fold_rev (roundup thy' cons export)
         (registrations_of context' loc) (Idents.get context', []);
-  in
-    thy'
-    |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
-  end;
+    fun add_dep dep = add_registration {dep = dep, mixin = NONE, export = export};
+  in thy' |> fold_rev (Context.theory_map o add_dep) regs end;
 
 
 (*** Storing results ***)
 
 fun add_facts loc kind facts ctxt =