# HG changeset patch
# User blanchet
# Date 1283514844 -7200
# Node ID 611e41ef07c31e4f552491c99e77f8d3ad53f0d7
# Parent  2e9bdc6fbedf6ad5c88c67dd55baae8d106b7d0f
disable "definitional CNF";
it has a bad impact on "Metis_Examples". Perhaps we should use it more selectively, based on how many clauses we would get using the naive method

diff -r 2e9bdc6fbedf -r 611e41ef07c3 src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Sep 03 13:45:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Fri Sep 03 13:54:04 2010 +0200
@@ -241,7 +241,7 @@
   let
     val ctxt0 = Variable.global_thm_context th
     val (nnf_th, ctxt) = to_nnf th ctxt0
-    val def_th = to_definitional_cnf_with_quantifiers thy nnf_th
+    val def_th = (* FIXME: to_definitional_cnf_with_quantifiers thy *) nnf_th
     val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs def_th)
     val (cnf_ths, ctxt) = Meson.make_cnf sko_ths def_th ctxt
   in
diff -r 2e9bdc6fbedf -r 611e41ef07c3 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Sep 03 13:45:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Sep 03 13:54:04 2010 +0200
@@ -798,6 +798,7 @@
     val thy = ProofContext.theory_of ctxt
     val _ = trace_msg (fn () =>
         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
+val timer = Timer.startRealTimer () (*###*)
   in
     if exists_type type_has_top_sort (prop_of st0) then
       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
@@ -806,6 +807,9 @@
                   (maps neg_clausify)
                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
                   ctxt i st0
+|> tap (fn _ => priority (" METIS " ^
+cat_lines (map (Display.string_of_thm ctxt) ths) ^
+string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ " ms")) (*###*)
   end
 
 val metis_tac = generic_metis_tac HO