src/HOL/Tools/Meson/meson.ML

            (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
     handle THM ("tryres", _, _) => th
   else th
 
 fun unfold_set_const_simps ctxt =
-  if Config.get ctxt unfold_set_consts then @{thms Collect_def_raw mem_def_raw}
+  if Config.get ctxt unfold_set_consts then []
   else []
 
 (*The simplification removes defined quantifiers and occurrences of True and False.
   nnf_ss also includes the one-point simprocs,
   which are needed to avoid the various one-point theorems from generating junk clauses.*)