proper dynamic position of application context, e.g. relevant for 'global_interpretation';

--- a/src/Pure/Isar/spec_rules.ML	Mon Dec 02 15:30:17 2019 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Mon Dec 02 16:15:27 2019 +0100
@@ -159,13 +159,11 @@
 (* add *)
 
 fun add b rough_classification terms rules lthy =
-  let
-    val pos = Position.thread_data ();
-    val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules);
-  in
+  let val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules) in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
       (fn phi => fn context =>
         let
+          val pos = Position.thread_data ();
           val name = Name_Space.full_name (Name_Space.naming_of context) (Morphism.binding phi b);
           val (terms', rules') =
             map (Thm.transfer (Context.theory_of context)) thms0