# HG changeset patch # User haftmann # Date 1324739698 -3600 # Node ID 4c629115e3ab541715d21f0b6d096ea4f222aec0 # Parent af59825c40cf7f5893feaa9f82378bf8e61823d3 dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw` diff -r af59825c40cf -r 4c629115e3ab 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.