# HG changeset patch
# User blanchet
# Date 1325611998 -3600
# Node ID 4bf24b90703c596d8e580fb6524be1634a6aeaf6
# Parent  287a3cefc21b309bbcbdb5bd58964eb35a1f2ebe
tuning

diff -r 287a3cefc21b -r 4bf24b90703c src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jan 03 18:33:18 2012 +0100
@@ -1093,12 +1093,11 @@
       | _ => do_term bs t
   in do_formula [] end
 
-fun presimplify_term _ [] t = t
-  | presimplify_term ctxt presimp_consts t =
-    t |> exists_Const (member (op =) presimp_consts o fst) t
-         ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
-            #> Meson.presimplify ctxt
-            #> prop_of)
+fun presimplify_term ctxt t =
+  t |> exists_Const (member (op =) Meson.presimplified_consts o fst) t
+       ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
+          #> Meson.presimplify
+          #> prop_of)
 
 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
 fun conceal_bounds Ts t =
@@ -1196,7 +1195,7 @@
       | freeze t = t
   in t |> exists_subterm is_Var t ? freeze end
 
-fun presimp_prop ctxt presimp_consts role t =
+fun presimp_prop ctxt role t =
   (let
      val thy = Proof_Context.theory_of ctxt
      val t = t |> Envir.beta_eta_contract
@@ -1206,7 +1205,7 @@
    in
      t |> need_trueprop ? HOLogic.mk_Trueprop
        |> extensionalize_term ctxt
-       |> presimplify_term ctxt presimp_consts
+       |> presimplify_term ctxt
        |> HOLogic.dest_Trueprop
    end
    handle TERM _ => if role = Conjecture then @{term False} else @{term True})
@@ -1708,7 +1707,6 @@
   let
     val thy = Proof_Context.theory_of ctxt
     val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
-    val presimp_consts = Meson.presimplified_consts ctxt
     val fact_ts = facts |> map snd
     (* Remove existing facts from the conjecture, as this can dramatically
        boost an ATP's performance (for some reason). *)
@@ -1722,8 +1720,7 @@
       |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
     val ((conjs, facts), lam_facts) =
       (conjs, facts)
-      |> presimp
-         ? pairself (map (apsnd (uncurry (presimp_prop ctxt presimp_consts))))
+      |> presimp ? pairself (map (apsnd (uncurry (presimp_prop ctxt))))
       |> (if lam_trans = no_lamsN then
             rpair []
           else
diff -r 287a3cefc21b -r 4bf24b90703c src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Tue Jan 03 18:33:18 2012 +0100
@@ -18,8 +18,8 @@
     thm list -> thm -> Proof.context
     -> Proof.context -> thm list * Proof.context
   val finish_cnf: thm list -> thm list
-  val presimplified_consts : Proof.context -> string list
-  val presimplify: Proof.context -> thm -> thm
+  val presimplified_consts : string list
+  val presimplify: 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
@@ -578,18 +578,18 @@
     addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq},
                  @{simproc let_simp}]
 
-fun presimplified_consts ctxt =
+val presimplified_consts =
   [@{const_name simp_implies}, @{const_name False}, @{const_name True},
    @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}, @{const_name If},
    @{const_name Let}]
 
-fun presimplify ctxt =
+val presimplify =
   rewrite_rule (map safe_mk_meta_eq nnf_simps)
   #> simplify nnf_ss
   #> Raw_Simplifier.rewrite_rule @{thms Let_def_raw}
 
 fun make_nnf ctxt th = case prems_of th of
-    [] => th |> presimplify ctxt |> make_nnf1 ctxt
+    [] => th |> presimplify |> make_nnf1 ctxt
   | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
 
 fun choice_theorems thy =