"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))

--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Wed Sep 29 23:30:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Wed Sep 29 23:55:14 2010 +0200
@@ -7,13 +7,12 @@
 
 signature MESON_CLAUSIFY =
 sig
-  val new_skolemizer : bool Config.T
   val new_skolem_var_prefix : string
   val extensionalize_theorem : thm -> thm
   val introduce_combinators_in_cterm : cterm -> thm
   val introduce_combinators_in_theorem : thm -> thm
   val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
-  val cnf_axiom : theory -> thm -> thm option * thm list
+  val cnf_axiom : theory -> bool -> thm -> thm option * thm list
   val meson_general_tac : Proof.context -> thm list -> int -> tactic
   val setup: theory -> theory
 end;
@@ -21,9 +20,6 @@
 structure Meson_Clausify : MESON_CLAUSIFY =
 struct
 
-val (new_skolemizer, new_skolemizer_setup) =
-  Attrib.config_bool "meson_new_skolemizer" (K false)
-
 val new_skolem_var_prefix = "SK?" (* purposedly won't parse *)
 
 (**** Transformation of Elimination Rules into First-Order Formulas****)
@@ -306,10 +302,9 @@
   end
 
 (* Convert a theorem to CNF, with additional premises due to skolemization. *)
-fun cnf_axiom thy th =
+fun cnf_axiom thy new_skolemizer th =
   let
     val ctxt0 = Variable.global_thm_context th
-    val new_skolemizer = Config.get ctxt0 new_skolemizer
     val (opt, nnf_th, ctxt) = nnf_axiom new_skolemizer th ctxt0
     fun aux th =
       Meson.make_cnf (if new_skolemizer then
@@ -338,12 +333,11 @@
   let
     val thy = ProofContext.theory_of ctxt
     val ctxt0 = Classical.put_claset HOL_cs ctxt
-  in Meson.meson_tac ctxt0 (maps (snd o cnf_axiom thy) ths) end
+  in Meson.meson_tac ctxt0 (maps (snd o cnf_axiom thy false) ths) end
 
 val setup =
-  new_skolemizer_setup
-  #> Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
-       SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
-       "MESON resolution proof procedure"
+  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
+     SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
+     "MESON resolution proof procedure"
 
 end;

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Sep 29 23:30:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Sep 29 23:55:14 2010 +0200
@@ -11,6 +11,7 @@
 sig
   val trace : bool Unsynchronized.ref
   val type_lits : bool Config.T
+  val new_skolemizer : bool Config.T
   val metis_tac : Proof.context -> thm list -> int -> tactic
   val metisF_tac : Proof.context -> thm list -> int -> tactic
   val metisFT_tac : Proof.context -> thm list -> int -> tactic
@@ -25,7 +26,9 @@
 
 fun trace_msg msg = if !trace then tracing (msg ()) else ()
 
-val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
+val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
+val (new_skolemizer, new_skolemizer_setup) =
+  Attrib.config_bool "metis_new_skolemizer" (K false)
 
 fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
 
@@ -147,9 +150,10 @@
 fun FOL_SOLVE mode ctxt cls ths0 =
   let val thy = ProofContext.theory_of ctxt
       val type_lits = Config.get ctxt type_lits
+      val new_skolemizer = Config.get ctxt new_skolemizer
       val th_cls_pairs =
-        map (fn th => (Thm.get_name_hint th, Meson_Clausify.cnf_axiom thy th))
-            ths0
+        map (fn th => (Thm.get_name_hint th,
+                       Meson_Clausify.cnf_axiom thy new_skolemizer th)) ths0
       val thss = map (snd o snd) th_cls_pairs
       val dischargers = map_filter (fst o snd) th_cls_pairs
       val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
@@ -271,6 +275,7 @@
 
 val setup =
   type_lits_setup
+  #> new_skolemizer_setup
   #> method @{binding metis} HO "Metis for FOL/HOL problems"
   #> method @{binding metisF} FO "Metis for FOL problems"
   #> method @{binding metisFT} FT