# HG changeset patch
# User blanchet
# Date 1284055783 -7200
# Node ID a56f931fffff7d4b71e18aea103b79e1a21efbe5
# Parent  c663b0cdebc411815b9411bf70df954c0dc31d14
use the Meson cutoff as the cutoff for using definitional CNF -- it's simpler that way

diff -r c663b0cdebc4 -r a56f931fffff src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Thu Sep 09 18:53:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Thu Sep 09 20:09:43 2010 +0200
@@ -7,7 +7,6 @@
 
 signature CLAUSIFIER =
 sig
-  val min_clauses_for_definitional_cnf : int
   val extensionalize_theorem : thm -> thm
   val introduce_combinators_in_cterm : cterm -> thm
   val introduce_combinators_in_theorem : thm -> thm
@@ -18,11 +17,6 @@
 structure Clausifier : CLAUSIFIER =
 struct
 
-(* Cutoff beyond which definitional CNF is used. Definitional CNF has a certain
-   overhead, but it prevents the exponential explosion of the number of
-   clauses. *)
-val min_clauses_for_definitional_cnf = 30
-
 (**** Transformation of Elimination Rules into First-Order Formulas****)
 
 val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
@@ -252,12 +246,8 @@
                      th ctxt
     val (cnf_ths, ctxt) =
       aux nnf_th
-      |> (fn (cnf_ths, ctxt) =>
-             if null cnf_ths orelse
-                length cnf_ths >= min_clauses_for_definitional_cnf then
-               aux (to_definitional_cnf_with_quantifiers thy nnf_th)
-             else
-               (cnf_ths, ctxt))
+      |> (fn ([], _) => aux (to_definitional_cnf_with_quantifiers thy nnf_th)
+           | p => p)
   in
     cnf_ths |> map introduce_combinators_in_theorem
             |> Variable.export ctxt ctxt0