src/HOL/Decision_Procs/Commutative_Ring.thy

 
 context cring
 begin
 
 local_setup \<open>
-Local_Theory.declaration {syntax = false, pervasive = false}
+Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
   (fn phi => Ring_Tac.Ring_Simps.map (Ring_Tac.insert_rules Ring_Tac.eq_ring_simps
     (Morphism.term phi \<^term>\<open>R\<close>,
      (Morphism.fact phi @{thms Ipol.simps [meta] Ipol_Pc [meta]},
       Morphism.fact phi @{thms Ipolex.simps [meta] Ipolex_Const [meta]},
       Morphism.fact phi @{thms Ipolex_polex_list.simps [meta]},