# HG changeset patch
# User blanchet
# Date 1305274243 -7200
# Node ID 4b7a988a021361f4885dfd380183dc89d8b8e0ac
# Parent  be6164bc97449133e7efcb5c51e559389356139b
optimized a common case

diff -r be6164bc9744 -r 4b7a988a0213 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 13 10:10:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 13 10:10:43 2011 +0200
@@ -607,16 +607,18 @@
 
 fun filter_type_args _ _ _ [] = []
   | filter_type_args thy s arity T_args =
-    let
-      val U = s |> Sign.the_const_type thy (* may throw "TYPE" *)
-      val res_U = U |> chop_fun arity |> snd
-      val res_U_vars = Term.add_tvarsT res_U []
-      val U_args = (s, U) |> Sign.const_typargs thy
-    in
-      U_args ~~ T_args
-      |> map_filter (fn (U, T) =>
-                        if member (op =) res_U_vars (dest_TVar U) then SOME T
-                        else NONE)
+    let val U = s |> Sign.the_const_type thy (* may throw "TYPE" *) 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_filter (fn (U, T) =>
+                            if member (op =) res_U_vars (dest_TVar U) then
+                              SOME T
+                            else
+                              NONE)
+        end
     end
     handle TYPE _ => T_args