dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`
authorhaftmann
Sat, 24 Dec 2011 16:14:58 +0100
changeset 45981 4c629115e3ab
parent 45980 af59825c40cf
child 45982 989b1eede03c
dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`
src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Sat Dec 24 16:14:58 2011 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Sat Dec 24 16:14:58 2011 +0100
@@ -569,7 +569,7 @@
   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.