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 -