src/HOL/Tools/meson.ML
 changeset 24742 73b8b42a36b6 parent 24300 e170cee91c66 child 24827 646bdc51eb7d
```     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
```