src/Pure/Isar/local_theory.ML

   val notes: Attrib.fact list -> local_theory -> (string * thm list) list * local_theory
   val notes_kind: string -> Attrib.fact list -> local_theory ->
     (string * thm list) list * local_theory
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
-  val declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration ->
+  val declaration: {syntax: bool, pervasive: bool, pos: Position.T} -> Morphism.declaration ->
     local_theory -> local_theory
   val theory_registration: Locale.registration -> local_theory -> local_theory
   val locale_dependency: Locale.registration -> local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory

  {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory,
   notes: string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory,
   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
-  declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration_entity ->
+  declaration: {syntax: bool, pervasive: bool, pos: Position.T} -> Morphism.declaration_entity ->
     local_theory -> local_theory,
   theory_registration: Locale.registration -> local_theory -> local_theory,
   locale_dependency: Locale.registration -> local_theory -> local_theory,
   pretty: local_theory -> Pretty.T list};
 

   |> background_theory_result (fn thy => thy
       |> Global_Theory.add_thms_dynamic' (Sign.inherit_naming thy lthy) (binding, f))
   |-> (fn name =>
     map_contexts (fn _ => fn ctxt =>
       Proof_Context.transfer_facts (Proof_Context.theory_of ctxt) ctxt) #>
-    declaration {syntax = false, pervasive = false} (fn phi =>
+    declaration {syntax = false, pervasive = false, pos = Binding.pos_of binding} (fn phi =>
       let val binding' = Morphism.binding phi binding in
         Context.mapping
           (Global_Theory.alias_fact binding' name)
           (Proof_Context.alias_fact binding' name)
       end));
 
 
 (* default sort *)
 
 fun set_defsort S =
-  declaration {syntax = true, pervasive = false}
+  declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
     (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
 
 
 (* syntax *)
 

   let
     val args = map (fn (c, T, mx) => (c, prep_type lthy T, mx)) raw_args;
     val args' = map (fn (c, T, mx) => (c, T, Mixfix.reset_pos mx)) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.syntax add mode args;
   in
-    declaration {syntax = true, pervasive = false}
+    declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
       (fn _ => Proof_Context.generic_syntax add mode args') lthy
   end;
 
 val syntax = gen_syntax (K I);
 val syntax_cmd = gen_syntax Proof_Context.read_typ_syntax;

     val prepare = prep_type lthy #> Logic.type_map (Assumption.export_term lthy (target_of lthy));
     val args = map (apfst prepare) raw_args;
     val args' = map (apsnd Mixfix.reset_pos) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.type_notation add mode args;
   in
-    declaration {syntax = true, pervasive = false}
+    declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
       (Proof_Context.generic_type_notation add mode args') lthy
   end;
 
 fun gen_notation prep_const add mode raw_args lthy =
   let
     val prepare = prep_const lthy #> Assumption.export_term lthy (target_of lthy);
     val args = map (apfst prepare) raw_args;
     val args' = map (apsnd Mixfix.reset_pos) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.notation add mode args;
   in
-    declaration {syntax = true, pervasive = false}
+    declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
       (Proof_Context.generic_notation add mode args') lthy
   end;
 
 in
 

 
 
 (* name space aliases *)
 
 fun syntax_alias global_alias local_alias b name =
-  declaration {syntax = true, pervasive = false} (fn phi =>
+  declaration {syntax = true, pervasive = false, pos = Position.thread_data ()} (fn phi =>
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);
 
 val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
 val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;