src/HOL/Tools/record.ML

   - 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>
    {lhss = [\<^term>\<open>x::'a::{}\<close>],
+    passive = false,
     proc = fn _ => fn ctxt => fn ct =>
       let
         val thy = Proof_Context.theory_of ctxt;
         val t = Thm.term_of ct;
       in

   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>
    {lhss = [\<^term>\<open>x::'a::{}\<close>],
+    passive = false,
     proc = fn _ => fn ctxt => fn ct =>
       let
         val thy = Proof_Context.theory_of ctxt;
         val t = Thm.term_of ct;
         (*We can use more-updators with other updators as long

  Complexity: #components * #updates     #updates
 *)
 
 val  _ = Theory.setup (Named_Target.theory_map (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> =>
           (case rec_id ~1 T of
             "" => NONE

           else NONE
       | _ => NONE)};
 
 val  _ = Theory.setup (Named_Target.theory_map (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;
         val t = Thm.term_of ct;
         fun mkeq (lr, T, (sel, Tsel), x) i =