1.1 --- a/src/HOL/Tools/meson.ML	Fri Dec 22 20:58:14 2006 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Fri Dec 22 21:00:42 2006 +0100
     1.3 @@ -193,7 +193,7 @@
     1.4  
     1.5  (*** The basic CNF transformation ***)
     1.6  
     1.7 -val max_clauses = ref 20;
     1.8 +val max_clauses = ref 40;
     1.9  
    1.10  fun sum x y = if x < !max_clauses andalso y < !max_clauses then x+y else !max_clauses;
    1.11  fun prod x y = if x < !max_clauses andalso y < !max_clauses then x*y else !max_clauses;
    1.12 @@ -648,7 +648,7 @@
    1.13  
    1.14  (*Top-level conversion to meta-level clauses. Each clause has  
    1.15    leading !!-bound universal variables, to express generality. To get 
    1.16 -  disjunctions instead of meta-clauses, remove "make_meta_clauses" below.*)
    1.17 +  meta-clauses instead of disjunctions, uncomment "make_meta_clauses" below.*)
    1.18  val make_clauses_tac = 
    1.19    SUBGOAL
    1.20      (fn (prop,_) =>
    1.21 @@ -658,7 +658,7 @@
    1.22  	    (fn hyps => 
    1.23                (Method.insert_tac
    1.24                  (map forall_intr_vars 
    1.25 -                  (make_meta_clauses (make_clauses hyps))) 1)),
    1.26 +                  ( (**make_meta_clauses**) (make_clauses hyps))) 1)),
    1.27  	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    1.28       end);
    1.29