src/HOL/Tools/Meson/meson.ML
changeset 45981 4c629115e3ab
parent 45740 132a3e1c0fe5
child 46071 1613933e412c
     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.