dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`
authorhaftmann
Sat Dec 24 16:14:58 2011 +0100 (2011-12-24)
changeset 459814c629115e3ab
parent 45980 af59825c40cf
child 45982 989b1eede03c
dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`
src/HOL/Tools/Meson/meson.ML
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Sat Dec 24 16:14:58 2011 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sat Dec 24 16:14:58 2011 +0100
     1.3 @@ -569,7 +569,7 @@
     1.4    else th
     1.5  
     1.6  fun unfold_set_const_simps ctxt =
     1.7 -  if Config.get ctxt unfold_set_consts then @{thms Collect_def_raw mem_def_raw}
     1.8 +  if Config.get ctxt unfold_set_consts then []
     1.9    else []
    1.10  
    1.11  (*The simplification removes defined quantifiers and occurrences of True and False.