src/Pure/Isar/theory_target.ML

       (case pairself Term.head_of (rhs, rhs') of
         (Const (a, _), Const (a', _)) => a = a'
       | _ => false);
   in
     eq_heads ? (Context.mapping_result
-      (Sign.add_abbrev Syntax.internalM arg') (ProofContext.add_abbrev Syntax.internalM arg')
+      (Sign.add_abbrev Syntax.internalM [] arg') (ProofContext.add_abbrev Syntax.internalM [] arg')
     #-> (fn (lhs, _) =>
       Term.equiv_types (rhs, rhs') ?
         Morphism.form (ProofContext.target_notation prmode [(lhs, mx)])))
   end;
 
-fun internal_abbrev prmode ((c, mx), t) =
+fun internal_abbrev prmode ((c, mx), t) lthy = lthy
   (* FIXME really permissive *)
-  LocalTheory.term_syntax (perhaps o try o target_abbrev prmode ((c, mx), t))
-  #> ProofContext.add_abbrev Syntax.internalM (c, t) #> snd;
+  |> LocalTheory.term_syntax (perhaps o try o target_abbrev prmode ((c, mx), t))
+  |> ProofContext.add_abbrev Syntax.internalM (ContextPosition.properties_of lthy) (c, t)
+  |> snd;
 
 fun consts is_loc some_class depends decls lthy =
   let
     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
 
     fun const ((c, T), mx) thy =
       let
         val U = map #2 xs ---> T;
         val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
         val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
-        val thy' = Sign.add_consts_authentic [(c, U, mx1)] thy;
+        val thy' = Sign.add_consts_authentic (ContextPosition.properties_of lthy) [(c, U, mx1)] thy;
       in (((c, mx2), t), thy') end;
 
     fun const_class (SOME class) ((c, _), mx) (_, t) =
           Class.add_const_in_class class ((c, t), mx)
       | const_class NONE _ _ = I;

     val xs = map Free (occ_params target [t]);
     val u = fold_rev Term.lambda xs t;
     val U = Term.fastype_of u;
     val u' = singleton (Variable.export_terms (Variable.declare_term u target) thy_ctxt) u;
 
-    val ((lhs as Const (full_c, _), rhs), lthy1) = lthy
-      |> LocalTheory.theory_result (Sign.add_abbrev (#1 prmode) (c, u'));
+    val ((lhs as Const (full_c, _), rhs), lthy1) = lthy |> LocalTheory.theory_result
+      (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u'));
     val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
   in
     lthy1
     |> LocalTheory.theory (Sign.add_notation prmode [(lhs, mx1)])
     |> is_loc ? internal_abbrev prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs))

 
     (*thm definition*)
     val result = th''
       |> PureThy.name_thm true true ""
       |> Goal.close_result
+      |> fold PureThy.tag_rule (ContextPosition.properties_of ctxt)
       |> PureThy.name_thm true true name;
 
     (*import fixes*)
     val (tvars, vars) =
       chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs)