# HG changeset patch
# User blanchet
# Date 1280434395 -7200
# Node ID e3bb96b83807fa4824f5d0d9d40f9981cd7b49b4
# Parent  db90d313cf53d2d24f1d47eb27702cb2ba8d271b
fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)

diff -r db90d313cf53 -r e3bb96b83807 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jul 29 21:20:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jul 29 22:13:15 2010 +0200
@@ -86,11 +86,11 @@
             val args   = map hol_term_to_fol_FO tms
         in Metis.Term.Fn (c, tyargs @ args) end
     | (CombVar ((v, _), _), []) => Metis.Term.Var v
-    | _ => raise Fail "hol_term_to_fol_FO";
+    | _ => raise METIS ("hol_term_to_fol_FO", "non first-order combterm")
 
-fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
-  | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
+fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
       Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist)
+  | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
   | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
        Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
 
@@ -662,7 +662,7 @@
    ("c_False", (true, @{thms True_or_False})),
    ("c_If", (true, @{thms if_True if_False True_or_False}))]
 
-fun is_quasi_fol_clause thy =
+fun is_quasi_fol_clause thy th =
   Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
 
 (* Function to generate metis clauses, including comb and type clauses *)
@@ -797,10 +797,8 @@
          if mode = HO then
            (warning ("Metis: Falling back on \"metisFT\".");
             generic_metis_tac FT ctxt ths i st0)
-         else if msg = "" then
+         else
            Seq.empty
-         else
-           raise error ("Metis (" ^ loc ^ "): " ^ msg)
 
 val metis_tac = generic_metis_tac HO
 val metisF_tac = generic_metis_tac FO
diff -r db90d313cf53 -r e3bb96b83807 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Jul 29 21:20:24 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Jul 29 22:13:15 2010 +0200
@@ -390,10 +390,13 @@
 
 fun sort_clauses ths = sort (make_ord fewerlits) ths;
 
-(*True if the given type contains bool anywhere*)
-fun has_bool (Type("bool",_)) = true
-  | has_bool (Type(_, Ts)) = exists has_bool Ts
-  | has_bool _ = false;
+fun has_bool @{typ bool} = true
+  | has_bool (Type (_, Ts)) = exists has_bool Ts
+  | has_bool _ = false
+
+fun has_fun (Type (@{type_name fun}, _)) = true
+  | has_fun (Type (_, Ts)) = exists has_fun Ts
+  | has_fun _ = false
 
 (*Is the string the name of a connective? Really only | and Not can remain,
   since this code expects to be called on a clause form.*)
@@ -405,7 +408,7 @@
   of any argument contains bool.*)
 val has_bool_arg_const =
     exists_Const
-      (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
+      (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T));
 
 (*A higher-order instance of a first-order constant? Example is the definition of
   one, 1, at a function type in theory SetsAndFunctions.*)
@@ -418,8 +421,9 @@
   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_subterm (fn Var (_, T) => has_bool T | _ => false) t  orelse
-         has_bool_arg_const t  orelse
+    not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
+                           | _ => false) t orelse
+         has_bool_arg_const t orelse
          exists_Const (higher_inst_const thy) t orelse
          has_meta_conn t);