# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 7384b771805debf0d2a2881f5cd165cab1a83e3e
# Parent  007117fed1831c025f331dafacd87d466ee262db
made "explicit_apply"'s smart mode (more) complete

diff -r 007117fed183 -r 7384b771805d 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
@@ -1046,8 +1046,11 @@
     fun consider_var_arity const_T var_T max_ary =
       let
         fun iter ary T =
-          if ary = max_ary orelse type_instance ctxt (var_T, T) then ary
-          else iter (ary + 1) (range_type T)
+          if ary = max_ary orelse type_instance ctxt (var_T, T) orelse
+             type_instance ctxt (T, var_T) then
+            ary
+          else
+            iter (ary + 1) (range_type T)
       in iter 0 const_T end
     fun add_var_or_bound_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
       if explicit_apply = NONE andalso
@@ -1287,8 +1290,7 @@
     @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
         by (unfold fdisj_def) fast+}),
    (("fimplies", false),
-    @{lemma "P | fimplies P Q" "~ Q | fimplies P Q"
-            "~ fimplies P Q | ~ P | Q"
+    @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
         by (unfold fimplies_def) fast+}),
    (("If", true), @{thms if_True if_False True_or_False})]
   |> map (apsnd (map zero_var_indexes))