# HG changeset patch
# User wenzelm
# Date 1684861159 -7200
# Node ID 838198d17a40e4972c33d2c5301d1140b421e11d
# Parent  bc42c074e58f2a3bf435777ec0447970799425d9
tuned;

diff -r bc42c074e58f -r 838198d17a40 src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue May 23 18:46:15 2023 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue May 23 18:59:19 2023 +0200
@@ -942,16 +942,15 @@
 context cring
 begin
 
-local_setup \<open>
-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
+declaration \<open>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]},
       Morphism.fact phi @{thms in_carrier_Nil in_carrier_Cons},
       singleton (Morphism.fact phi) @{thm head.simps(2) [meta]},
-      singleton (Morphism.fact phi) @{thm norm_subst_correct [meta]}))))
+      singleton (Morphism.fact phi) @{thm norm_subst_correct [meta]})))
 \<close>
 
 end
diff -r bc42c074e58f -r 838198d17a40 src/HOL/Decision_Procs/Reflective_Field.thy
--- a/src/HOL/Decision_Procs/Reflective_Field.thy	Tue May 23 18:46:15 2023 +0200
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Tue May 23 18:59:19 2023 +0200
@@ -909,15 +909,14 @@
 context field
 begin
 
-local_setup \<open>
-Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
-  (fn phi => Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps
+declaration \<open>fn phi =>
+  Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps
     (Morphism.term phi \<^term>\<open>R\<close>,
      (Morphism.fact phi @{thms feval.simps [meta] feval_Cnst [meta]},
       Morphism.fact phi @{thms peval.simps [meta] peval_Cnst [meta]},
       Morphism.fact phi @{thms nonzero.simps [meta] nonzero_singleton [meta]},
       singleton (Morphism.fact phi) @{thm nth_el_Cons [meta]},
-      singleton (Morphism.fact phi) @{thm feval_eq}))))
+      singleton (Morphism.fact phi) @{thm feval_eq})))
 \<close>
 
 end
diff -r bc42c074e58f -r 838198d17a40 src/HOL/Eisbach/Tests.thy
--- a/src/HOL/Eisbach/Tests.thy	Tue May 23 18:46:15 2023 +0200
+++ b/src/HOL/Eisbach/Tests.thy	Tue May 23 18:59:19 2023 +0200
@@ -432,9 +432,7 @@
   assumes A : "A"
 begin
 
-local_setup
-  \<open>Local_Theory.declaration {pervasive = false, syntax = false, pos = \<^here>}
-    (fn phi => Data.put (Morphism.fact phi @{thms A}))\<close>
+declaration \<open>fn phi => Data.put (Morphism.fact phi @{thms A})\<close>
 
 lemma A by dynamic_thms_test