# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 0c9bf1a8e0d805d92774646a57b17b54bd439c5d
# Parent  ca7b0a48515df527ac036f0f6dbebaf51a163c8b
make "smart" mode of "explicit_apply" smarter, by also detecting the other kind of higher-order quantification, namely "bool"s

diff -r ca7b0a48515d -r 0c9bf1a8e0d8 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -1049,44 +1049,51 @@
           if ary = max_ary orelse type_instance ctxt (var_T, T) then ary
           else iter (ary + 1) (range_type T)
       in iter 0 const_T end
-    fun add top_level tm (accum as (ho_var_Ts, sym_tab)) =
-      let
-        fun do_var_or_bound_var T =
-          if explicit_apply = NONE andalso can dest_funT T then
-            let
-              fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
-                {pred_sym = pred_sym,
-                 min_ary =
-                   fold (fn T' => consider_var_arity T' T) types min_ary,
-                 max_ary = max_ary, types = types}
-              val ho_var_Ts' = ho_var_Ts |> insert_type ctxt I T
-            in
-              if pointer_eq (ho_var_Ts', ho_var_Ts) then accum
-              else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab)
-            end
+    fun add_var_or_bound_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
+      if explicit_apply = NONE andalso
+         (can dest_funT T orelse T = @{typ bool}) then
+        let
+          val bool_vars' = bool_vars orelse body_type T = @{typ bool}
+          fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
+            {pred_sym = pred_sym andalso not bool_vars',
+             min_ary =
+               fold (fn T' => consider_var_arity T' T) types min_ary,
+             max_ary = max_ary, types = types}
+          val fun_var_Ts' =
+            fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
+        in
+          if bool_vars' = bool_vars andalso
+             pointer_eq (fun_var_Ts', fun_var_Ts) then
+            accum
           else
-            accum
-        val (head, args) = strip_combterm_comb tm
-      in
+            ((bool_vars', fun_var_Ts'),
+             Symtab.map (K repair_min_arity) sym_tab)
+        end
+      else
+        accum
+    fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
+      let val (head, args) = strip_combterm_comb tm in
         (case head of
            CombConst ((s, _), T, _) =>
            if String.isPrefix bound_var_prefix s then
-             do_var_or_bound_var T
+             add_var_or_bound_var T accum
            else
              let val ary = length args in
-               (ho_var_Ts,
+               ((bool_vars, fun_var_Ts),
                 case Symtab.lookup sym_tab s of
                   SOME {pred_sym, min_ary, max_ary, types} =>
                   let
+                    val pred_sym =
+                      pred_sym andalso top_level andalso not bool_vars
                     val types' = types |> insert_type ctxt I T
                     val min_ary =
                       if is_some explicit_apply orelse
                          pointer_eq (types', types) then
                         min_ary
                       else
-                        fold (consider_var_arity T) ho_var_Ts min_ary
+                        fold (consider_var_arity T) fun_var_Ts min_ary
                   in
-                    Symtab.update (s, {pred_sym = pred_sym andalso top_level,
+                    Symtab.update (s, {pred_sym = pred_sym,
                                        min_ary = Int.min (ary, min_ary),
                                        max_ary = Int.max (ary, max_ary),
                                        types = types'})
@@ -1094,19 +1101,20 @@
                   end
                 | NONE =>
                   let
+                    val pred_sym = top_level andalso not bool_vars
                     val min_ary =
                       case explicit_apply of
                         SOME true => 0
                       | SOME false => ary
-                      | NONE => fold (consider_var_arity T) ho_var_Ts ary
+                      | NONE => fold (consider_var_arity T) fun_var_Ts ary
                   in
-                    Symtab.update_new (s, {pred_sym = top_level,
+                    Symtab.update_new (s, {pred_sym = pred_sym,
                                            min_ary = min_ary, max_ary = ary,
                                            types = [T]})
                                       sym_tab
                   end)
              end
-         | CombVar (_, T) => do_var_or_bound_var T
+         | CombVar (_, T) => add_var_or_bound_var T accum
          | _ => accum)
         |> fold (add false) args
       end
@@ -1124,8 +1132,8 @@
    |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
 
 fun sym_table_for_facts ctxt explicit_apply facts =
-  Symtab.empty
-  |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
+  ((false, []), Symtab.empty)
+  |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
   |> fold Symtab.update default_sym_tab_entries
 
 fun min_arity_of sym_tab s =