src/HOL/Tools/Meson/meson.ML
changeset 51717 9e7d1c139569
parent 50702 70c2a6d513fd
child 52230 1105b3b5aa77
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4      -> Proof.context -> thm list * Proof.context
     1.5    val finish_cnf: thm list -> thm list
     1.6    val presimplified_consts : string list
     1.7 -  val presimplify: thm -> thm
     1.8 +  val presimplify: Proof.context -> thm -> thm
     1.9    val make_nnf: Proof.context -> thm -> thm
    1.10    val choice_theorems : theory -> thm list
    1.11    val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
    1.12 @@ -541,22 +541,23 @@
    1.13  (* FIXME: "let_simp" is probably redundant now that we also rewrite with
    1.14    "Let_def [abs_def]". *)
    1.15  val nnf_ss =
    1.16 -  HOL_basic_ss addsimps nnf_extra_simps
    1.17 +  simpset_of (put_simpset HOL_basic_ss @{context}
    1.18 +    addsimps nnf_extra_simps
    1.19      addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
    1.20 -                 @{simproc let_simp}]
    1.21 +                 @{simproc let_simp}])
    1.22  
    1.23  val presimplified_consts =
    1.24    [@{const_name simp_implies}, @{const_name False}, @{const_name True},
    1.25     @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}, @{const_name If},
    1.26     @{const_name Let}]
    1.27  
    1.28 -val presimplify =
    1.29 +fun presimplify ctxt =
    1.30    rewrite_rule (map safe_mk_meta_eq nnf_simps)
    1.31 -  #> simplify nnf_ss
    1.32 +  #> simplify (put_simpset nnf_ss ctxt)
    1.33    #> Raw_Simplifier.rewrite_rule @{thms Let_def [abs_def]}
    1.34  
    1.35  fun make_nnf ctxt th = case prems_of th of
    1.36 -    [] => th |> presimplify |> make_nnf1 ctxt
    1.37 +    [] => th |> presimplify ctxt |> make_nnf1 ctxt
    1.38    | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
    1.39  
    1.40  fun choice_theorems thy =