src/HOL/Tools/Meson/meson.ML
changeset 42750 c8b1d9ee3758
parent 42747 f132d13fcf75
child 42760 d83802e7348e
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
     1.5    val finish_cnf: thm list -> thm list
     1.6    val unfold_set_const_simps : Proof.context -> thm 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 @@ -577,11 +577,15 @@
    1.13    HOL_basic_ss addsimps nnf_extra_simps
    1.14      addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq}, @{simproc let_simp}];
    1.15  
    1.16 -val presimplify =
    1.17 -  rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss
    1.18 +fun presimplify ctxt =
    1.19 +  rewrite_rule (map safe_mk_meta_eq nnf_simps)
    1.20 +  #> simplify nnf_ss
    1.21 +  (* TODO: avoid introducing "Set.member" in "Ball_def" "Bex_def" above if and
    1.22 +     when "metis_unfold_set_consts" becomes the only mode of operation. *)
    1.23 +  #> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
    1.24  
    1.25  fun make_nnf ctxt th = case prems_of th of
    1.26 -    [] => th |> presimplify |> make_nnf1 ctxt
    1.27 +    [] => th |> presimplify ctxt |> make_nnf1 ctxt
    1.28    | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
    1.29  
    1.30  fun choice_theorems thy =