more careful treatment position: existing facts refer to interpretation command, future facts refer to themselves (see also 4270da306442);

--- a/src/Pure/Isar/interpretation.ML	Thu Aug 30 14:38:24 2018 +0200
+++ b/src/Pure/Isar/interpretation.ML	Thu Aug 30 14:48:02 2018 +0200
@@ -100,7 +100,7 @@
 fun abs_def_rule eqns ctxt =
   (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
 
-fun note_eqns_register pos note add_registration
+fun note_eqns_register note add_registration
     deps eqnss witss def_eqns thms export export' ctxt =
   let
     val factss = thms
@@ -112,10 +112,7 @@
     val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule;
     val deps' =
       (deps ~~ witss) |> map (fn ((dep, morph), wits) =>
-        let val morph' = morph
-          $> Element.satisfy_morphism (map (Element.transform_witness export') wits)
-          $> Morphism.binding_morphism "position" (Binding.set_pos pos)
-        in (dep, morph') end);
+        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)));
     fun register (dep, eqns) ctxt =
       ctxt |> add_registration
         {dep = dep,
@@ -132,9 +129,8 @@
   let
     val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) =
       prep_interpretation expression raw_defs initial_ctxt;
-    val pos = Position.thread_data ();
     fun after_qed witss eqns =
-      note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns export export';
+      note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export';
   in setup_proof after_qed propss (flat eq_propss) goal_ctxt end;
 
 end;

--- a/src/Pure/Isar/locale.ML	Thu Aug 30 14:38:24 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 30 14:48:02 2018 +0200
@@ -542,6 +542,7 @@
 fun add_registration {dep = (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 = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
     val morph = base_morph $> mix;
     val inst = instance_of thy name morph;
@@ -557,7 +558,7 @@
       (* add mixin *)
       |> amend_registration {dep = (name, morph), mixin = mixin, export = export}
       (* activate import hierarchy as far as not already active *)
-      |> activate_facts (SOME export) (name, morph)
+      |> activate_facts (SOME export) (name, morph $> pos_morph)
   end;
 
 val add_registration_theory = Context.theory_map o add_registration;