# HG changeset patch
# User wenzelm
# Date 1575299727 -3600
# Node ID e64c249d3d98b8db8e23684fde95f75a7412e37c
# Parent  37eb175895c50a3913c38812b018a69d50e18f90
proper dynamic position of application context, e.g. relevant for 'global_interpretation';

diff -r 37eb175895c5 -r e64c249d3d98 src/Pure/Isar/spec_rules.ML
--- 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