src/HOL/Tools/Meson/meson.ML
changeset 46093 4bf24b90703c
parent 46071 1613933e412c
child 46503 186f4cab2ba0
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Jan 03 18:33:18 2012 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Jan 03 18:33:18 2012 +0100
     1.3 @@ -18,8 +18,8 @@
     1.4      thm list -> thm -> Proof.context
     1.5      -> Proof.context -> thm list * Proof.context
     1.6    val finish_cnf: thm list -> thm list
     1.7 -  val presimplified_consts : Proof.context -> string list
     1.8 -  val presimplify: Proof.context -> thm -> thm
     1.9 +  val presimplified_consts : string list
    1.10 +  val presimplify: thm -> thm
    1.11    val make_nnf: Proof.context -> thm -> thm
    1.12    val choice_theorems : theory -> thm list
    1.13    val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
    1.14 @@ -578,18 +578,18 @@
    1.15      addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
    1.16                   @{simproc let_simp}]
    1.17  
    1.18 -fun presimplified_consts ctxt =
    1.19 +val presimplified_consts =
    1.20    [@{const_name simp_implies}, @{const_name False}, @{const_name True},
    1.21     @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}, @{const_name If},
    1.22     @{const_name Let}]
    1.23  
    1.24 -fun presimplify ctxt =
    1.25 +val presimplify =
    1.26    rewrite_rule (map safe_mk_meta_eq nnf_simps)
    1.27    #> simplify nnf_ss
    1.28    #> Raw_Simplifier.rewrite_rule @{thms Let_def_raw}
    1.29  
    1.30  fun make_nnf ctxt th = case prems_of th of
    1.31 -    [] => th |> presimplify ctxt |> make_nnf1 ctxt
    1.32 +    [] => th |> presimplify |> make_nnf1 ctxt
    1.33    | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
    1.34  
    1.35  fun choice_theorems thy =