src/HOL/Tools/Meson/meson.ML
changeset 46904 f30e941b4512
parent 46818 2a28e66e2e4c
child 47022 8eac39af4ec0
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Mar 13 16:22:18 2012 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Mar 13 16:40:06 2012 +0100
     1.3 @@ -560,7 +560,7 @@
     1.4  val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
     1.5  
     1.6  (* FIXME: "let_simp" is probably redundant now that we also rewrite with
     1.7 -  "Let_def_raw". *)
     1.8 +  "Let_def [abs_def]". *)
     1.9  val nnf_ss =
    1.10    HOL_basic_ss addsimps nnf_extra_simps
    1.11      addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
    1.12 @@ -574,7 +574,7 @@
    1.13  val presimplify =
    1.14    rewrite_rule (map safe_mk_meta_eq nnf_simps)
    1.15    #> simplify nnf_ss
    1.16 -  #> Raw_Simplifier.rewrite_rule @{thms Let_def_raw}
    1.17 +  #> Raw_Simplifier.rewrite_rule @{thms Let_def [abs_def]}
    1.18  
    1.19  fun make_nnf ctxt th = case prems_of th of
    1.20      [] => th |> presimplify |> make_nnf1 ctxt