1.1 --- a/src/HOL/Tools/meson.ML	Thu Sep 27 17:28:05 2007 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Thu Sep 27 17:55:28 2007 +0200
     1.3 @@ -209,10 +209,10 @@
     1.4  
     1.5  (*** The basic CNF transformation ***)
     1.6  
     1.7 -val max_clauses = ref 40;
     1.8 +val max_clauses = 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 +fun sum x y = if x < max_clauses andalso y < max_clauses then x+y else max_clauses;
    1.13 +fun prod x y = if x < max_clauses andalso y < max_clauses then x*y else max_clauses;
    1.14  
    1.15  (*Estimate the number of clauses in order to detect infeasible theorems*)
    1.16  fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
    1.17 @@ -239,7 +239,7 @@
    1.18  
    1.19  val nclauses = signed_nclauses true;
    1.20  
    1.21 -fun too_many_clauses t = nclauses t >= !max_clauses;
    1.22 +fun too_many_clauses t = nclauses t >= max_clauses;
    1.23  
    1.24  (*Replaces universally quantified variables by FREE variables -- because
    1.25    assumptions may not contain scheme variables.  Later, we call "generalize". *)
    1.26 @@ -396,7 +396,7 @@
    1.27        [] => false (*not a function type, OK*)
    1.28      | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
    1.29  
    1.30 -(*Raises an exception if any Vars in the theorem mention type bool.
    1.31 +(*Returns false if any Vars in the theorem mention type bool.
    1.32    Also rejects functions whose arguments are Booleans or other functions.*)
    1.33  fun is_fol_term thy t =
    1.34      Term.is_first_order ["all","All","Ex"] t andalso