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