# HG changeset patch
# User blanchet
# Date 1310649277 -7200
# Node ID 048619bb1dc3e269632997ea978d2767edd70864
# Parent  d439173f3daf81f0eb5bf3a43d9d2e78dc921592
always unfold "Let"s is Sledgehammer, Metis, and MESON

diff -r d439173f3daf -r 048619bb1dc3 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Thu Jul 14 15:14:37 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Thu Jul 14 15:14:37 2011 +0200
@@ -575,6 +575,8 @@
          if_eq_cancel cases_simp}
 val nnf_extra_simps = @{thms split_ifs ex_simps all_simps simp_thms}
 
+(* FIXME: "let_simp" is probably redundant now that we also rewrite with
+  "Let_def_raw". *)
 val nnf_ss =
   HOL_basic_ss addsimps nnf_extra_simps
     addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
@@ -592,7 +594,8 @@
   #> simplify nnf_ss
   (* TODO: avoid introducing "Set.member" in "Ball_def" "Bex_def" above if and
      when "metis_unfold_set_consts" becomes the only mode of operation. *)
-  #> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
+  #> Raw_Simplifier.rewrite_rule
+         (@{thm Let_def_raw} :: unfold_set_const_simps ctxt)
 
 fun make_nnf ctxt th = case prems_of th of
     [] => th |> presimplify ctxt |> make_nnf1 ctxt