src/HOL/Tools/Meson/meson.ML
changeset 52230 1105b3b5aa77
parent 51717 9e7d1c139569
child 54742 7a86358a3c0b
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu May 30 08:27:51 2013 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu May 30 12:35:40 2013 +0200
     1.3 @@ -554,7 +554,7 @@
     1.4  fun presimplify ctxt =
     1.5    rewrite_rule (map safe_mk_meta_eq nnf_simps)
     1.6    #> simplify (put_simpset nnf_ss ctxt)
     1.7 -  #> Raw_Simplifier.rewrite_rule @{thms Let_def [abs_def]}
     1.8 +  #> rewrite_rule @{thms Let_def [abs_def]}
     1.9  
    1.10  fun make_nnf ctxt th = case prems_of th of
    1.11      [] => th |> presimplify ctxt |> make_nnf1 ctxt