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