clarified signature: more concise variations on implicit theory setup;

--- a/src/Doc/Codegen/Computations.thy	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Doc/Codegen/Computations.thy	Wed Oct 18 15:13:52 2023 +0200
@@ -276,8 +276,7 @@
     \<^instantiate>\<open>x = ct and y = \<open>if b then \<^cterm>\<open>True\<close> else \<^cterm>\<open>False\<close>\<close>
       in cterm \<open>x \<equiv> y\<close> for x y :: bool\<close>;
 
-  val (_, dvd_oracle) = Context.>>> (Context.map_theory_result
-    (Thm.add_oracle (\<^binding>\<open>dvd\<close>, raw_dvd)));
+  val (_, dvd_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\<open>dvd\<close>, raw_dvd));
 
   in
 

--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Wed Oct 18 15:13:52 2023 +0200
@@ -663,8 +663,7 @@
   \<^instantiate>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
     in cterm \<open>x \<equiv> y\<close> for x y :: pol\<close>;
 
-val (_, raw_pol_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (\<^binding>\<open>pnsubstl\<close>, pol)));
+val (_, raw_pol_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\<open>pnsubstl\<close>, pol));
 
 fun pol_oracle ctxt ct t = raw_pol_oracle (ctxt, ct, t);
 

--- a/src/HOL/Decision_Procs/Reflective_Field.thy	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Wed Oct 18 15:13:52 2023 +0200
@@ -643,8 +643,7 @@
   \<^instantiate>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
     in cterm \<open>x \<equiv> y\<close> for x y :: \<open>pexpr \<times> pexpr \<times> pexpr list\<close>\<close>;
 
-val (_, raw_fnorm_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (\<^binding>\<open>fnorm\<close>, fnorm)));
+val (_, raw_fnorm_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\<open>fnorm\<close>, fnorm));
 
 fun fnorm_oracle ctxt ct t = raw_fnorm_oracle (ctxt, ct, t);
 

--- a/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/compute.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -339,8 +339,8 @@
 
 fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
 
-val (_, export_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (\<^binding>\<open>compute\<close>, fn (thy, hyps, shyps, prop) =>
+val (_, export_oracle) =
+  Theory.setup_result (Thm.add_oracle (\<^binding>\<open>compute\<close>, fn (thy, hyps, shyps, prop) =>
     let
         val shyptab = add_shyps shyps Sorttab.empty
         fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
@@ -355,7 +355,7 @@
           else ()
     in
         Thm.global_cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop)
-    end)));
+    end));
 
 fun export_thm thy hyps shyps prop =
     let

--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -194,8 +194,8 @@
         set_inducts = []}}
   end;
 
-val _ = Theory.setup (Named_Target.theory_map (fn lthy =>
+val _ = Named_Target.global_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));
+    [fp_sugar_of_sum, fp_sugar_of_prod] lthy);
 
 end;

--- a/src/HOL/Tools/Qelim/cooper.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -697,11 +697,11 @@
 
 end;
 
-val (_, oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (\<^binding>\<open>cooper\<close>,
+val (_, oracle) =
+  Theory.setup_result (Thm.add_oracle (\<^binding>\<open>cooper\<close>,
     (fn (ctxt, t) =>
       (Thm.cterm_of ctxt o Logic.mk_equals o apply2 HOLogic.mk_Trueprop)
-        (t, procedure t)))));
+        (t, procedure t))));
 
 val comp_ss =
   simpset_of (put_simpset HOL_ss \<^context> addsimps @{thms semiring_norm});

--- a/src/HOL/Tools/record.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/HOL/Tools/record.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -1060,7 +1060,7 @@
   - If X is a more-selector we have to make sure that S is not in the updated
     subrecord.
 *)
-val  _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\<open>select_update\<close>
+val  _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\<open>select_update\<close>
    {lhss = [\<^term>\<open>x::'a::{}\<close>],
     passive = false,
     proc = fn _ => fn ctxt => fn ct =>
@@ -1115,7 +1115,7 @@
               end
             else NONE
         | _ => NONE)
-      end}));
+      end});
 
 val simproc =
   #2 (Simplifier.check_simproc (Context.the_local_context ()) ("select_update", Position.none));
@@ -1165,7 +1165,7 @@
   In both cases "more" updates complicate matters: for this reason
   we omit considering further updates if doing so would introduce
   both a more update and an update to a field within it.*)
-val  _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\<open>update\<close>
+val  _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\<open>update\<close>
    {lhss = [\<^term>\<open>x::'a::{}\<close>],
     passive = false,
     proc = fn _ => fn ctxt => fn ct =>
@@ -1283,7 +1283,7 @@
             (prove_unfold_defs thy upd_funs noops' [simproc]
               (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
         else NONE
-      end}));
+      end});
 
 val upd_simproc =
   #2 (Simplifier.check_simproc (Context.the_local_context ()) ("update", Position.none));
@@ -1306,7 +1306,7 @@
  Complexity: #components * #updates     #updates
 *)
 
-val  _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\<open>eq\<close>
+val  _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\<open>eq\<close>
    {lhss = [\<^term>\<open>r = s\<close>],
     passive = false,
     proc = fn _ => fn ctxt => fn ct =>
@@ -1318,7 +1318,7 @@
               (case get_equalities (Proof_Context.theory_of ctxt) name of
                 NONE => NONE
               | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
-      | _ => NONE)}));
+      | _ => NONE)});
 
 val eq_simproc =
   #2 (Simplifier.check_simproc (Context.the_local_context ()) ("eq", Position.none));
@@ -1360,7 +1360,7 @@
           else NONE
       | _ => NONE)};
 
-val  _ = Theory.setup (Named_Target.theory_map (Simplifier.define_simproc \<^binding>\<open>ex_sel_eq\<close>
+val  _ = Named_Target.global_setup (Simplifier.define_simproc \<^binding>\<open>ex_sel_eq\<close>
    {lhss = [\<^term>\<open>Ex t\<close>],
     passive = false,
     proc = fn _ => fn ctxt => fn ct =>
@@ -1399,7 +1399,7 @@
                     addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
             end handle TERM _ => NONE)
         | _ => NONE)
-      end}));
+      end});
 
 val ex_sel_eq_simproc =
   #2 (Simplifier.check_simproc (Context.the_local_context ()) ("ex_sel_eq", Position.none));

--- a/src/HOL/Types_To_Sets/local_typedef.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/HOL/Types_To_Sets/local_typedef.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -70,8 +70,9 @@
 
 (** END OF THE CRITICAL CODE **)
 
-val (_, cancel_type_definition_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (\<^binding>\<open>cancel_type_definition\<close>, cancel_type_definition_cterm)));
+val (_, cancel_type_definition_oracle) =
+  Theory.setup_result
+    (Thm.add_oracle (\<^binding>\<open>cancel_type_definition\<close>, cancel_type_definition_cterm));
 
 fun cancel_type_definition thm =
   Drule.implies_elim_list (cancel_type_definition_oracle thm) (map Thm.assume (Thm.chyps_of thm));

--- a/src/HOL/Types_To_Sets/unoverloading.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/HOL/Types_To_Sets/unoverloading.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -119,9 +119,9 @@
 
 (** END OF THE CRITICAL CODE **)
 
-val (_, unoverload_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (\<^binding>\<open>unoverload\<close>,
-  fn (const, thm) => unoverload_impl const  thm)));
+val (_, unoverload_oracle) =
+  Theory.setup_result
+    (Thm.add_oracle (\<^binding>\<open>unoverload\<close>, fn (const, thm) => unoverload_impl const  thm));
 
 fun unoverload const thm = unoverload_oracle (const, thm);
 

--- a/src/HOL/ex/Sorting_Algorithms_Examples.thy	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/HOL/ex/Sorting_Algorithms_Examples.thy	Wed Oct 18 15:13:52 2023 +0200
@@ -27,8 +27,7 @@
     \<^instantiate>\<open>x = ct and y = \<open>Thm.cterm_of ctxt (term_of_int_list ks)\<close>
       in cterm \<open>x \<equiv> y\<close> for x y :: \<open>int list\<close>\<close>;
 
-  val (_, sort_oracle) = Context.>>> (Context.map_theory_result
-    (Thm.add_oracle (\<^binding>\<open>sort\<close>, raw_sort)));
+  val (_, sort_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\<open>sort\<close>, raw_sort));
 
 in
 

--- a/src/Pure/Isar/isar_cmd.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -117,10 +117,9 @@
     (ML_Lex.read "val " @
      ML_Lex.read_range range name @
      ML_Lex.read
-      (" = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (" ^
+      (" = snd (Theory.setup_result (Thm.add_oracle (" ^
         ML_Syntax.make_binding (name, #1 range) ^ ", ") @
-     ML_Lex.read_source source @
-     ML_Lex.read "))))")
+     ML_Lex.read_source source @ ML_Lex.read ")))")
   |> Context.theory_map;
 
 

--- a/src/Pure/Isar/named_target.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Pure/Isar/named_target.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -16,6 +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 revoke_reinitializability: local_theory -> local_theory
   val exit_global_reinitialize: local_theory -> (theory -> local_theory) * theory
 end;
@@ -139,8 +142,11 @@
 val theory_init = init [] "";
 
 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;
 
-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;
 
 val revoke_reinitializability = (Data.map o Option.map o apsnd) (K false);
 

--- a/src/Pure/ML/ml_thms.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Pure/ML/ml_thms.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -122,8 +122,7 @@
 fun ml_store get (name, ths) =
   let
     val (_, ths') =
-      Context.>>> (Context.map_theory_result
-        (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])])));
+      Theory.setup_result (Global_Theory.note_thms "" ((Binding.name name, []), [(ths, [])]));
     val _ = Theory.setup (Data.put ths');
     val _ =
       if name = "" then ()

--- a/src/Pure/Tools/plugin.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Pure/Tools/plugin.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -57,13 +57,13 @@
     val thy' = Data.put data' thy;
   in (name, thy') end;
 
-fun define_setup binding rhs = Context.>>> (Context.map_theory_result (define binding rhs));
+fun define_setup binding rhs = Theory.setup_result (define binding rhs);
 
 
 (* immediate entries *)
 
 fun declare binding thy = define binding [] thy;
-fun declare_setup binding = Context.>>> (Context.map_theory_result (declare binding));
+fun declare_setup binding = Theory.setup_result (declare binding);
 
 
 (* filter *)

--- a/src/Pure/drule.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Pure/drule.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -337,10 +337,10 @@
 val read_prop = certify o Simple_Syntax.read_prop;
 
 fun store_thm name th =
-  Context.>>> (Context.map_theory_result (Global_Theory.store_thm (name, th)));
+  Theory.setup_result (Global_Theory.store_thm (name, th));
 
 fun store_thm_open name th =
-  Context.>>> (Context.map_theory_result (Global_Theory.store_thm_open (name, th)));
+  Theory.setup_result (Global_Theory.store_thm_open (name, th));
 
 fun store_standard_thm name th = store_thm name (export_without_context th);
 fun store_standard_thm_open name th = store_thm_open name (export_without_context_open th);

--- a/src/Pure/ex/Def.thy	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Pure/ex/Def.thy	Wed Oct 18 15:13:52 2023 +0200
@@ -66,7 +66,7 @@
 (* simproc setup *)
 
 val _ =
-  (Theory.setup o Named_Target.theory_map)
+  Named_Target.global_setup
     (Simplifier.define_simproc \<^binding>\<open>expand_def\<close>
       {lhss = [Free ("x", TFree ("'a", []))], passive = false, proc = K get_def});
 

--- a/src/Pure/skip_proof.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Pure/skip_proof.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -26,8 +26,7 @@
 (* oracle setup *)
 
 val (_, make_thm_cterm) =
-  Context.>>>
-    (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", \<^here>), I)));
+  Theory.setup_result (Thm.add_oracle (Binding.make ("skip_proof", \<^here>), I));
 
 fun make_thm thy prop = make_thm_cterm (Thm.global_cterm_of thy prop);
 

--- a/src/Pure/theory.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Pure/theory.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -10,7 +10,9 @@
   val ancestors_of: theory -> theory list
   val nodes_of: theory -> theory list
   val setup: (theory -> theory) -> unit
+  val setup_result: (theory -> 'a * theory) -> 'a
   val local_setup: (Proof.context -> Proof.context) -> unit
+  val local_setup_result: (Proof.context -> 'a * Proof.context) -> 'a
   val install_pure: theory -> unit
   val get_pure: unit -> theory
   val get_pure_bootstrap: unit -> theory
@@ -49,7 +51,10 @@
 fun nodes_of thy = thy :: ancestors_of thy;
 
 fun setup f = Context.>> (Context.map_theory f);
+fun setup_result f = Context.>>> (Context.map_theory_result f);
+
 fun local_setup f = Context.>> (Context.map_proof f);
+fun local_setup_result f = Context.>>> (Context.map_proof_result f);
 
 
 (* implicit theory Pure *)

--- a/src/Tools/Code/code_runtime.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Tools/Code/code_runtime.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -152,9 +152,9 @@
     Thm.mk_binop iff ct (if result then \<^cprop>\<open>PROP Code_Generator.holds\<close> else ct)
   end;
 
-val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (\<^binding>\<open>holds_by_evaluation\<close>,
-  fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct)));
+val (_, raw_check_holds_oracle) =
+  Theory.setup_result (Thm.add_oracle (\<^binding>\<open>holds_by_evaluation\<close>,
+    fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct));
 
 fun check_holds_oracle ctxt evaluator vs_ty_t ct =
   raw_check_holds_oracle (ctxt, evaluator, vs_ty_t, ct);
@@ -417,8 +417,7 @@
 fun holds ct = Thm.mk_binop \<^cterm>\<open>Pure.eq :: prop \<Rightarrow> prop \<Rightarrow> prop\<close>
   ct \<^cprop>\<open>PROP Code_Generator.holds\<close>;
 
-val (_, holds_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (\<^binding>\<open>holds\<close>, holds)));
+val (_, holds_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\<open>holds\<close>, holds));
 
 in
 

--- a/src/Tools/nbe.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Tools/nbe.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -78,9 +78,9 @@
 
 val get_triv_classes = map fst o Triv_Class_Data.get;
 
-val (_, triv_of_class) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (\<^binding>\<open>triv_of_class\<close>, fn (thy, T, class) =>
-    Thm.global_cterm_of thy (Logic.mk_of_class (T, class)))));
+val (_, triv_of_class) =
+  Theory.setup_result (Thm.add_oracle (\<^binding>\<open>triv_of_class\<close>,
+    fn (thy, T, class) => Thm.global_cterm_of thy (Logic.mk_of_class (T, class))));
 
 in
 
@@ -592,10 +592,10 @@
     val rhs = Thm.cterm_of ctxt raw_rhs;
   in Thm.mk_binop eq lhs rhs end;
 
-val (_, raw_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (\<^binding>\<open>normalization_by_evaluation\<close>,
+val (_, raw_oracle) =
+  Theory.setup_result (Thm.add_oracle (\<^binding>\<open>normalization_by_evaluation\<close>,
     fn (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct) =>
-      mk_equals ctxt ct (normalize_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps))));
+      mk_equals ctxt ct (normalize_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps)));
 
 fun oracle nbe_program_idx_tab ctxt vs_ty_t deps ct =
   raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct);