src/HOL/Tools/record.ML

   - If S is a more-selector we have to make sure that the update on component
     X does not affect the selected subrecord.
   - 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 =>
       let
         val thy = Proof_Context.theory_of ctxt;

                         (Logic.list_all (vars, Logic.mk_equals (sel $ trm, trm'))))
                 | NONE => NONE)
               end
             else NONE
         | _ => NONE)
-      end}));
+      end});
 
 val simproc =
   #2 (Simplifier.check_simproc (Context.the_local_context ()) ("select_update", Position.none));
 
 fun get_upd_acc_cong_thm upd acc thy ss =

     (2)  "r(|M:= M r|) = r"
 
   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 =>
       let
         val thy = Proof_Context.theory_of ctxt;

         if simp orelse commuted then
           SOME
             (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));
 
 end;

 
              eq_simproc          split_simp_tac
  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 =>
       (case Thm.term_of ct of
         \<^Const_>\<open>HOL.eq T for _ _\<close> =>

             "" => NONE
           | name =>
               (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));
 
 

                   else NONE
                 end)
           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 =>
       let
         val thy = Proof_Context.theory_of ctxt;

                 (fn {context = ctxt', ...} =>
                   simp_tac (put_simpset (get_simpset thy) ctxt'
                     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));
 
 val _ = Theory.setup (map_theory_simpset (fn ctxt => ctxt delsimprocs [ex_sel_eq_simproc]));