# HG changeset patch
# User blanchet
# Date 1307385394 -7200
# Node ID 839f599bc7ed945cfcdf93ffb4603dd37073e208
# Parent  68e3cd19fee849d99bd719a2eabb18ba9cea1b0c
ensured that the logic for "explicit_apply = smart" also works on CNF (i.e. new Metis)

diff -r 68e3cd19fee8 -r 839f599bc7ed src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -1045,24 +1045,28 @@
           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 val (head, args) = strip_combterm_comb tm in
+      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
+          else
+            accum
+        val (head, args) = strip_combterm_comb tm
+      in
         (case head of
            CombConst ((s, _), T, _) =>
            if String.isPrefix bound_var_prefix s then
-             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
-             else
-               accum
+             do_var_or_bound_var T
            else
              let val ary = length args in
                (ho_var_Ts,
@@ -1097,6 +1101,7 @@
                                       sym_tab
                   end)
              end
+         | CombVar (_, T) => do_var_or_bound_var T
          | _ => accum)
         |> fold (add false) args
       end