src/Pure/Isar/locale.ML

   val intro_add: attribute
   val unfold_add: attribute
   val intro_locales_tac: {strict: bool, eager: bool} -> Proof.context -> thm list -> tactic
 
   (* Registrations and dependencies *)
-  type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism}
+  type registration = {inst: 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 add_registration_theory: registration -> theory -> theory
   val add_registration_proof: registration -> Proof.context -> Proof.context
   val add_registration_local_theory: registration -> local_theory -> local_theory

 (*** Add and extend registrations ***)
 
 type registration = Locale.registration;
 
 fun amend_registration {mixin = NONE, ...} context = context
-  | amend_registration {dep = (name, morph), mixin = SOME mixin, export} context =
+  | amend_registration {inst = (name, morph), mixin = SOME mixin, export} context =
       let
         val thy = Context.theory_of context;
         val ctxt = Context.proof_of context;
 
         val regs = get_regs 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 {dep = (name, base_morph), mixin, export} context =
+fun add_registration {inst = (name, base_morph), mixin, export} context =
   let
     val thy = Context.theory_of context;
     val pos_morph = Morphism.binding_morphism "position" (Binding.set_pos (Position.thread_data ()));
     val mix_morph = (case mixin of NONE => base_morph | SOME (mix, _) => base_morph $> mix);
     val inst = instance_of thy name mix_morph;

     else
       (idents, context)
       (* add new registrations with inherited mixins *)
       |> roundup thy (add_reg thy export) export (name, mix_morph) |> #2
       (* add mixin *)
-      |> amend_registration {dep = (name, mix_morph), mixin = mixin, export = export}
+      |> amend_registration {inst = (name, mix_morph), mixin = mixin, export = export}
       (* activate import hierarchy as far as not already active *)
       |> activate_facts (SOME export) (name, mix_morph $> pos_morph)
   end;
 
 val add_registration_theory = Context.theory_map o add_registration;

     name = loc ? cons (name, morphisms)) (get_regs context) []
   (*with inherited mixins*)
   |> map (fn (name, (base, export)) =>
       (name, base $> (collect_mixins context (name, base $> export)) $> export));
 
-fun add_dependency loc {dep = (name, morph), mixin, export} thy =
+fun add_dependency loc {inst = (name, morph), mixin, export} thy =
   let
     val serial' = serial ();
     val thy' = thy |>
       (change_locale loc o apsnd)
         (apfst (cons ((name, (morph, export)), serial')) #>

     val (_, regs) =
       fold_rev (roundup thy' cons export)
         (registrations_of context' loc) (Idents.get context', []);
   in
     thy'
-    |> fold_rev (fn dep => add_registration_theory {dep = dep, mixin = NONE, export = export}) regs
+    |> fold_rev (fn dep => add_registration_theory {inst = dep, mixin = NONE, export = export}) regs
   end;
 
 
 (*** Storing results ***)