# HG changeset patch
# User wenzelm
# Date 1697707816 -7200
# Node ID 200daaab2578f22260926f72a58a042e8035f0a0
# Parent  fc598652fb8af121a1c1b0df31eef242b79b5dca
clarified signature: Named_Target.setup works both for global and local theory;

diff -r fc598652fb8a -r 200daaab2578 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Wed Oct 18 22:09:25 2023 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Thu Oct 19 11:30:16 2023 +0200
@@ -194,7 +194,7 @@
         set_inducts = []}}
   end;
 
-val _ = Named_Target.global_setup (fn lthy =>
+val _ = Named_Target.setup (fn lthy =>
   fold (BNF_FP_Def_Sugar.register_fp_sugars (K true) o single o (fn f => f lthy))
     [fp_sugar_of_sum, fp_sugar_of_prod] lthy);
 
diff -r fc598652fb8a -r 200daaab2578 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Oct 18 22:09:25 2023 +0200
+++ b/src/HOL/Tools/record.ML	Thu Oct 19 11:30:16 2023 +0200
@@ -1116,7 +1116,7 @@
   end;
 
 val simproc =
-  Simplifier.simproc_setup_global
+  Simplifier.simproc_setup
    {name = \<^binding>\<open>select_update\<close>, lhss = ["x::'a::{}"], proc = K select_update_proc,
      passive = false};
 
@@ -1284,7 +1284,7 @@
   end;
 
 val upd_simproc =
-  Simplifier.simproc_setup_global
+  Simplifier.simproc_setup
     {name = \<^binding>\<open>update\<close>, lhss = ["x::'a::{}"], proc = K upd_proc, passive = false};
 
 end;
@@ -1317,7 +1317,7 @@
   | _ => NONE);
 
 val eq_simproc =
-  Simplifier.simproc_setup_global
+  Simplifier.simproc_setup
     {name = \<^binding>\<open>eq\<close>, lhss = ["r = s"], proc = K eq_proc, passive = false};
 
 
@@ -1396,7 +1396,7 @@
   end;
 
 val ex_sel_eq_simproc =
-  Simplifier.simproc_setup_global
+  Simplifier.simproc_setup
     {name = \<^binding>\<open>ex_sel_eq\<close>, lhss = ["Ex t"], proc = K ex_sel_eq_proc, passive = true};
 
 
diff -r fc598652fb8a -r 200daaab2578 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Wed Oct 18 22:09:25 2023 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu Oct 19 11:30:16 2023 +0200
@@ -16,9 +16,9 @@
   val theory_map: (local_theory -> local_theory) -> theory -> theory
   val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) ->
     theory -> 'b * theory
-  val global_setup: (local_theory -> local_theory) -> unit
-  val global_setup_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> 'b
-  val global_setup_result0: (local_theory -> 'a * local_theory) -> 'a
+  val setup: (local_theory -> local_theory) -> unit
+  val setup_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) -> 'b
+  val setup_result0: (local_theory -> 'a * local_theory) -> 'a
   val revoke_reinitializability: local_theory -> local_theory
   val exit_global_reinitialize: local_theory -> (theory -> local_theory) * theory
 end;
@@ -144,9 +144,10 @@
 fun theory_map g = theory_init #> g #> Local_Theory.exit_global;
 fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f;
 
-val global_setup = Theory.setup o theory_map;
-fun global_setup_result f g = Theory.setup_result (theory_map_result f g);
-fun global_setup_result0 g = global_setup_result (K I) g;
+fun setup g = Context.>> (Context.mapping (theory_map g) g);
+fun setup_result f g =
+  Context.>>> (Context.mapping_result (theory_map_result f g) (g #>> f Morphism.identity));
+fun setup_result0 g = setup_result (K I) g;
 
 val revoke_reinitializability = (Data.map o Option.map o apsnd) (K false);
 
diff -r fc598652fb8a -r 200daaab2578 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Oct 18 22:09:25 2023 +0200
+++ b/src/Pure/Pure.thy	Thu Oct 19 11:30:16 2023 +0200
@@ -336,7 +336,7 @@
     (Simplifier.simproc_setup_parser >> (fn arg =>
       Context.proof_map
         (ML_Context.expression (Input.pos_of (#proc arg))
-          (ML_Lex.read "Simplifier.simproc_setup_local " @ Simplifier.simproc_setup_ml arg))));
+          (ML_Lex.read "Simplifier.simproc_setup " @ Simplifier.simproc_setup_ml arg))));
 
 in end\<close>
 
diff -r fc598652fb8a -r 200daaab2578 src/Pure/ex/Def.thy
--- a/src/Pure/ex/Def.thy	Wed Oct 18 22:09:25 2023 +0200
+++ b/src/Pure/ex/Def.thy	Thu Oct 19 11:30:16 2023 +0200
@@ -66,7 +66,7 @@
 (* simproc setup *)
 
 val _ =
-  Simplifier.simproc_setup_global
+  Simplifier.simproc_setup
     {name = \<^binding>\<open>expand_def\<close>, lhss = ["x::'a"], passive = false, proc = K get_def};
 
 
diff -r fc598652fb8a -r 200daaab2578 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Oct 18 22:09:25 2023 +0200
+++ b/src/Pure/simplifier.ML	Thu Oct 19 11:30:16 2023 +0200
@@ -48,8 +48,7 @@
   type simproc_setup_internal = (morphism -> Proof.context -> cterm -> thm option) simproc_setup
   val simproc_setup_parser: Input.source simproc_setup parser
   val simproc_setup_ml: Input.source simproc_setup -> ML_Lex.token Antiquote.antiquote list
-  val simproc_setup_local: simproc_setup_internal -> simproc
-  val simproc_setup_global: simproc_setup_internal -> simproc
+  val simproc_setup: simproc_setup_internal -> simproc
   val pretty_simpset: bool -> Proof.context -> Pretty.T
   val default_mk_sym: Proof.context -> thm -> thm option
   val prems_of: Proof.context -> thm list
@@ -190,12 +189,8 @@
      ", passive = " ^ Bool.toString passive ^
      ", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read ")}";
 
-fun simproc_setup_local ({name, lhss, passive, proc}: simproc_setup_internal) =
-  Theory.local_setup_result
-    (define_simproc_cmd name {lhss = lhss, passive = passive, proc = proc});
-
-fun simproc_setup_global ({name, lhss, passive, proc}: simproc_setup_internal) =
-  Named_Target.global_setup_result Raw_Simplifier.transform_simproc
+fun simproc_setup ({name, lhss, passive, proc}: simproc_setup_internal) =
+  Named_Target.setup_result Raw_Simplifier.transform_simproc
     (define_simproc_cmd name {lhss = lhss, passive = passive, proc = proc});