# HG changeset patch
# User wenzelm
# Date 1230678493 -3600
# Node ID 8615b4f540477f4f94e628f4a0ea12cbdf2c64c2
# Parent  4a478f9d2847c891a452b36b543d4a8e9188d599
use exists_subterm directly;

diff -r 4a478f9d2847 -r 8615b4f54047 src/HOL/Tools/meson.ML
--- 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;
-
diff -r 4a478f9d2847 -r 8615b4f54047 src/HOL/Tools/res_atp.ML
--- 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=().
diff -r 4a478f9d2847 -r 8615b4f54047 src/Provers/classical.ML
--- 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);