changeset 42455 | 6702c984bf5a |
parent 42361 | 23f352990944 |
child 42616 | 92715b528e78 |
--- a/src/HOL/Tools/Meson/meson.ML Fri Apr 22 13:07:47 2011 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Fri Apr 22 13:58:13 2011 +0200 @@ -567,7 +567,7 @@ val nnf_ss = HOL_basic_ss addsimps nnf_extra_simps - addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}]; + addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq}, @{simproc let_simp}]; val presimplify = rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss