merge

--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Sep 06 16:45:31 2011 +0900
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Sep 06 17:50:04 2011 +0900
@@ -263,7 +263,7 @@
       | str _ (ATyAbs (ss, ty)) =
         tptp_pi_binder ^ "[" ^
         commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types))
-                    ss) ^ "] : " ^ str false ty
+                    ss) ^ "]: " ^ str false ty
   in str true ty end
 
 fun string_for_type (THF0 _) ty = str_for_type ty
@@ -308,7 +308,7 @@
        | (_, true, [AAbs ((s', ty), tm)]) =>
          (*There is code in ATP_Translate to ensure that Eps is always applied
            to an abstraction*)
-         tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "] : " ^
+         tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
            string_for_term format tm ^ ""
          |> enclose "(" ")"
 
@@ -320,12 +320,12 @@
              s ^ "(" ^ commas ss ^ ")"
          end)
   | string_for_term (format as THF0 _) (AAbs ((s, ty), tm)) =
-    "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "] : " ^
+    "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
     string_for_term format tm ^ ")"
   | string_for_term _ _ = raise Fail "unexpected term in first-order format"
 and string_for_formula format (AQuant (q, xs, phi)) =
     string_for_quantifier q ^
-    "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
+    "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^
     string_for_formula format phi
     |> enclose "(" ")"
   | string_for_formula format

--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 16:45:31 2011 +0900
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 17:50:04 2011 +0900
@@ -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