1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu Jul 14 15:14:37 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu Jul 14 15:14:37 2011 +0200
     1.3 @@ -575,6 +575,8 @@
     1.4           if_eq_cancel cases_simp}
     1.5  val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
     1.6  
     1.7 +(* FIXME: "let_simp" is probably redundant now that we also rewrite with
     1.8 +  "Let_def_raw". *)
     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 @@ -592,7 +594,8 @@
    1.13    #> simplify nnf_ss
    1.14    (* TODO: avoid introducing "Set.member" in "Ball_def" "Bex_def" above if and
    1.15       when "metis_unfold_set_consts" becomes the only mode of operation. *)
    1.16 -  #> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
    1.17 +  #> Raw_Simplifier.rewrite_rule
    1.18 +         (@{thm Let_def_raw} :: unfold_set_const_simps ctxt)
    1.19  
    1.20  fun make_nnf ctxt th = case prems_of th of
    1.21      [] => th |> presimplify ctxt |> make_nnf1 ctxt