# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID c8b1d9ee375883bbbad105f479eef714aa8a9aad
# Parent  47f283fcf2ae155c329d91d324499e7182a63c17
ensure Set.member isn't introduced by Meson's preprocessing if it's supposed to be unfolded

diff -r 47f283fcf2ae -r c8b1d9ee3758 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
@@ -17,7 +17,7 @@
   val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
   val finish_cnf: thm list -> thm list
   val unfold_set_const_simps : Proof.context -> thm list
-  val presimplify: thm -> thm
+  val presimplify: Proof.context -> thm -> thm
   val make_nnf: Proof.context -> thm -> thm
   val choice_theorems : theory -> thm list
   val skolemize_with_choice_theorems : Proof.context -> thm list -> thm -> thm
@@ -577,11 +577,15 @@
   HOL_basic_ss addsimps nnf_extra_simps
     addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq}, @{simproc let_simp}];
 
-val presimplify =
-  rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss
+fun presimplify ctxt =
+  rewrite_rule (map safe_mk_meta_eq nnf_simps)
+  #> simplify nnf_ss
+  (* TODO: avoid introducing "Set.member" in "Ball_def" "Bex_def" above if and
+     when "metis_unfold_set_consts" becomes the only mode of operation. *)
+  #> Raw_Simplifier.rewrite_rule (unfold_set_const_simps ctxt)
 
 fun make_nnf ctxt th = case prems_of th of
-    [] => th |> presimplify |> make_nnf1 ctxt
+    [] => th |> presimplify ctxt |> make_nnf1 ctxt
   | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
 
 fun choice_theorems thy =
diff -r 47f283fcf2ae -r c8b1d9ee3758 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
@@ -345,7 +345,10 @@
       | _ => do_term bs t
   in do_formula [] end
 
-val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
+fun presimplify_term ctxt =
+  Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
+  #> Meson.presimplify ctxt
+  #> prop_of
 
 fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
 fun conceal_bounds Ts t =
@@ -424,7 +427,7 @@
               |> Raw_Simplifier.rewrite_term thy
                      (Meson.unfold_set_const_simps ctxt) []
               |> extensionalize_term ctxt
-              |> presimp ? presimplify_term thy
+              |> presimp ? presimplify_term ctxt
               |> perhaps (try (HOLogic.dest_Trueprop))
               |> introduce_combinators_in_term ctxt kind
               |> kind <> Axiom ? freeze_term