--- a/src/HOL/Tools/meson.ML Wed Dec 31 00:08:13 2008 +0100
+++ b/src/HOL/Tools/meson.ML Wed Dec 31 00:08:13 2008 +0100
@@ -1,11 +1,8 @@
(* Title: HOL/Tools/meson.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
The MESON resolution proof procedure for HOL.
-
-When making clauses, avoids using the rewriter -- instead uses RS recursively
+When making clauses, avoids using the rewriter -- instead uses RS recursively.
*)
signature MESON =
@@ -400,7 +397,7 @@
Also rejects functions whose arguments are Booleans or other functions.*)
fun is_fol_term thy t =
Term.is_first_order ["all","All","Ex"] t andalso
- not (exists (has_bool o fastype_of) (term_vars t) orelse
+ not (exists_subterm (fn Var (_, T) => has_bool T | _ => false) t orelse
has_bool_arg_const t orelse
exists_Const (higher_inst_const thy) t orelse
has_meta_conn t);
@@ -699,4 +696,3 @@
handle Subscript => Seq.empty;
end;
-
--- a/src/HOL/Tools/res_atp.ML Wed Dec 31 00:08:13 2008 +0100
+++ b/src/HOL/Tools/res_atp.ML Wed Dec 31 00:08:13 2008 +0100
@@ -1,7 +1,4 @@
-(* Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
- ID: $Id$
- Copyright 2004 University of Cambridge
-*)
+(* Author: Jia Meng, Cambridge University Computer Laboratory, NICTA *)
signature RES_ATP =
sig
@@ -507,11 +504,8 @@
fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
| is_taut _ = false;
-(*True if the term contains a variable whose (atomic) type is in the given list.*)
-fun has_typed_var tycons =
- let fun var_tycon (Var (_, Type(a,_))) = a mem_string tycons
- | var_tycon _ = false
- in exists var_tycon o term_vars end;
+fun has_typed_var tycons = exists_subterm
+ (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
(*Clauses are forbidden to contain variables of these types. The typical reason is that
they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
--- a/src/Provers/classical.ML Wed Dec 31 00:08:13 2008 +0100
+++ b/src/Provers/classical.ML Wed Dec 31 00:08:13 2008 +0100
@@ -1,7 +1,5 @@
(* Title: Provers/classical.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
Theorem prover for classical reasoning, including predicate calculus, set
theory, etc.
@@ -810,9 +808,7 @@
(fn (prem,i) =>
let val deti =
(*No Vars in the goal? No need to backtrack between goals.*)
- case term_vars prem of
- [] => DETERM
- | _::_ => I
+ if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I
in SELECT_GOAL (TRY (safe_tac cs) THEN
DEPTH_SOLVE (deti (depth_tac cs m 1))) i
end);