# HG changeset patch
# User blanchet
# Date 1315293068 -7200
# Node ID 1b333e4173a20452b9a3cae57427cc8ebd2ff953
# Parent  11a1290fd0acff3e96887bb5ec0860bfc3d36418
drop more type arguments soundly, when they can be deduced from the arg types

diff -r 11a1290fd0ac -r 1b333e4173a2 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Sep 05 17:45:37 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 09:11:08 2011 +0200
@@ -1369,16 +1369,14 @@
 
 fun filter_type_args _ _ _ [] = []
   | filter_type_args thy s arity T_args =
-    let val U = robust_const_type thy s in
-      case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
-        [] => []
-      | res_U_vars =>
-        let val U_args = (s, U) |> Sign.const_typargs thy in
-          U_args ~~ T_args
-          |> map (fn (U, T) =>
-                     if member (op =) res_U_vars (dest_TVar U) then T
-                     else dummyT)
-        end
+    let
+      val U = robust_const_type thy s
+      val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun arity |> fst) []
+      val U_args = (s, U) |> robust_const_typargs thy
+    in
+      U_args ~~ T_args
+      |> map (fn (U, T) =>
+                 if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
     end
     handle TYPE _ => T_args
 
@@ -1394,14 +1392,13 @@
          | SOME s'' =>
            let
              val s'' = invert_const s''
-             fun filtered_T_args false = T_args
-               | filtered_T_args true = filter_type_args thy s'' arity T_args
+             fun filter_T_args false = T_args
+               | filter_T_args true = filter_type_args thy s'' arity T_args
            in
              case type_arg_policy type_enc s'' of
-               Explicit_Type_Args drop_args =>
-               (name, filtered_T_args drop_args)
+               Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
              | Mangled_Type_Args drop_args =>
-               (mangled_const_name format type_enc (filtered_T_args drop_args)
+               (mangled_const_name format type_enc (filter_T_args drop_args)
                                    name, [])
              | No_Type_Args => (name, [])
            end)
@@ -1555,9 +1552,8 @@
   let
     fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
       | add (t $ u) = add t #> add u
-      | add (Const (x as (s, _))) =
-        if String.isPrefix skolem_const_prefix s then I
-        else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
+      | add (Const x) =
+        x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
       | add (Free (s, T)) =
         if String.isPrefix polymorphic_free_prefix s then
           T |> fold_type_constrs set_insert