1.1 --- a/src/HOL/Tools/meson.ML	Wed Dec 31 00:08:13 2008 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Dec 31 00:08:13 2008 +0100
     1.3 @@ -1,11 +1,8 @@
     1.4  (*  Title:      HOL/Tools/meson.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1992  University of Cambridge
     1.8  
     1.9  The MESON resolution proof procedure for HOL.
    1.10 -
    1.11 -When making clauses, avoids using the rewriter -- instead uses RS recursively
    1.12 +When making clauses, avoids using the rewriter -- instead uses RS recursively.
    1.13  *)
    1.14  
    1.15  signature MESON =
    1.16 @@ -400,7 +397,7 @@
    1.17    Also rejects functions whose arguments are Booleans or other functions.*)
    1.18  fun is_fol_term thy t =
    1.19      Term.is_first_order ["all","All","Ex"] t andalso
    1.20 -    not (exists (has_bool o fastype_of) (term_vars t)  orelse
    1.21 +    not (exists_subterm (fn Var (_, T) => has_bool T | _ => false) t  orelse
    1.22           has_bool_arg_const t  orelse
    1.23           exists_Const (higher_inst_const thy) t orelse
    1.24           has_meta_conn t);
    1.25 @@ -699,4 +696,3 @@
    1.26    handle Subscript => Seq.empty;
    1.27  
    1.28  end;
    1.29 -

     2.1 --- a/src/HOL/Tools/res_atp.ML	Wed Dec 31 00:08:13 2008 +0100
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Dec 31 00:08:13 2008 +0100
     2.3 @@ -1,7 +1,4 @@
     2.4 -(*  Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
     2.5 -    ID: $Id$
     2.6 -    Copyright 2004 University of Cambridge
     2.7 -*)
     2.8 +(*  Author: Jia Meng, Cambridge University Computer Laboratory, NICTA *)
     2.9  
    2.10  signature RES_ATP =
    2.11  sig
    2.12 @@ -507,11 +504,8 @@
    2.13  fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
    2.14    | is_taut _ = false;
    2.15  
    2.16 -(*True if the term contains a variable whose (atomic) type is in the given list.*)
    2.17 -fun has_typed_var tycons =
    2.18 -  let fun var_tycon (Var (_, Type(a,_))) = a mem_string tycons
    2.19 -        | var_tycon _ = false
    2.20 -  in  exists var_tycon o term_vars  end;
    2.21 +fun has_typed_var tycons = exists_subterm
    2.22 +  (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
    2.23  
    2.24  (*Clauses are forbidden to contain variables of these types. The typical reason is that
    2.25    they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().

     3.1 --- a/src/Provers/classical.ML	Wed Dec 31 00:08:13 2008 +0100
     3.2 +++ b/src/Provers/classical.ML	Wed Dec 31 00:08:13 2008 +0100
     3.3 @@ -1,7 +1,5 @@
     3.4  (*  Title:      Provers/classical.ML
     3.5 -    ID:         $Id$
     3.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 -    Copyright   1992  University of Cambridge
     3.8  
     3.9  Theorem prover for classical reasoning, including predicate calculus, set
    3.10  theory, etc.
    3.11 @@ -810,9 +808,7 @@
    3.12      (fn (prem,i) =>
    3.13        let val deti =
    3.14            (*No Vars in the goal?  No need to backtrack between goals.*)
    3.15 -          case term_vars prem of
    3.16 -              []        => DETERM
    3.17 -            | _::_      => I
    3.18 +          if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I
    3.19        in  SELECT_GOAL (TRY (safe_tac cs) THEN
    3.20                         DEPTH_SOLVE (deti (depth_tac cs m 1))) i
    3.21        end);