src/Pure/Isar/spec_rules.ML

--- a/src/Pure/Isar/spec_rules.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/spec_rules.ML	Tue May 23 18:46:15 2023 +0200
@@ -162,7 +162,7 @@
     val n = length terms;
     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}
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = Binding.pos_of b}
       (fn phi => fn context =>
         let
           val psi = Morphism.set_trim_context'' context phi;