src/HOL/Tools/Meson/meson.ML
changeset 54742 7a86358a3c0b
parent 52230 1105b3b5aa77
child 55990 41c6b99c5fb7
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -552,9 +552,9 @@
     1.4     @{const_name Let}]
     1.5  
     1.6  fun presimplify ctxt =
     1.7 -  rewrite_rule (map safe_mk_meta_eq nnf_simps)
     1.8 +  rewrite_rule ctxt (map safe_mk_meta_eq nnf_simps)
     1.9    #> simplify (put_simpset nnf_ss ctxt)
    1.10 -  #> rewrite_rule @{thms Let_def [abs_def]}
    1.11 +  #> rewrite_rule ctxt @{thms Let_def [abs_def]}
    1.12  
    1.13  fun make_nnf ctxt th = case prems_of th of
    1.14      [] => th |> presimplify ctxt |> make_nnf1 ctxt
    1.15 @@ -706,7 +706,7 @@
    1.16    Function mkcl converts theorems to clauses.*)
    1.17  fun MESON preskolem_tac mkcl cltac ctxt i st =
    1.18    SELECT_GOAL
    1.19 -    (EVERY [Object_Logic.atomize_prems_tac 1,
    1.20 +    (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
    1.21              rtac ccontr 1,
    1.22              preskolem_tac,
    1.23              Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>