# HG changeset patch
# User wenzelm
# Date 1537811000 -7200
# Node ID f4fb93197670e17b7dc14075f1270526a2d61ac8
# Parent  56c6378ebaeabaa892f2147b4edaadee13217fdb
tuned signature;

diff -r 56c6378ebaea -r f4fb93197670 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Sep 24 19:34:14 2018 +0200
+++ b/src/Pure/Isar/class.ML	Mon Sep 24 19:43:20 2018 +0200
@@ -233,7 +233,7 @@
       fold (fn cls => fn thy =>
         Context.theory_map
           (Locale.amend_registration
-            {dep = (cls, base_morphism thy cls),
+            {inst = (cls, base_morphism thy cls),
               mixin = SOME (eq_morph, true),
               export = export_morphism thy cls}) thy) (heritage thy [class]) thy
   | NONE => thy);
@@ -492,7 +492,7 @@
       (case some_dep_morph of
         SOME dep_morph =>
           Generic_Target.locale_dependency sub
-            {dep = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)),
+            {inst = (sup, dep_morph $> Element.satisfy_morphism (the_list some_witn)),
               mixin = NONE, export = export}
       | NONE => I);
   in
diff -r 56c6378ebaea -r f4fb93197670 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Mon Sep 24 19:34:14 2018 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Mon Sep 24 19:43:20 2018 +0200
@@ -329,7 +329,7 @@
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
        Locale.add_registration_theory
-         {dep = (class, base_morph),
+         {inst = (class, base_morph),
            mixin = Option.map (rpair true) eq_morph,
            export = export_morph}
     #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
diff -r 56c6378ebaea -r f4fb93197670 src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Mon Sep 24 19:34:14 2018 +0200
+++ b/src/Pure/Isar/interpretation.ML	Mon Sep 24 19:43:20 2018 +0200
@@ -115,7 +115,7 @@
         (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)));
     fun register (dep, eqns) ctxt =
       ctxt |> add_registration
-        {dep = dep,
+        {inst = dep,
           mixin =
             Option.map (rpair true)
               (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')),
diff -r 56c6378ebaea -r f4fb93197670 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Sep 24 19:34:14 2018 +0200
+++ b/src/Pure/Isar/local_theory.ML	Mon Sep 24 19:43:20 2018 +0200
@@ -16,7 +16,7 @@
 
 structure Locale =
 struct
-  type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism};
+  type registration = {inst: string * morphism, mixin: (morphism * bool) option, export: morphism};
 end;
 
 signature LOCAL_THEORY =
diff -r 56c6378ebaea -r f4fb93197670 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Sep 24 19:34:14 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Sep 24 19:43:20 2018 +0200
@@ -75,7 +75,7 @@
   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
@@ -539,7 +539,7 @@
 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;
@@ -561,7 +561,7 @@
 (* 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 ()));
@@ -575,7 +575,7 @@
       (* 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;
@@ -604,7 +604,7 @@
   |> 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 |>
@@ -617,7 +617,7 @@
         (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;