# HG changeset patch # User blanchet # Date 1305274243 -7200 # Node ID be6164bc97449133e7efcb5c51e559389356139b # Parent 7b14bafe6778c7e6672a1c0e249dab4001c0c40a avoid "UnequalLengths" exception for special constant "fequal" -- and optimize code in the common case where no type arguments are needed diff -r 7b14bafe6778 -r be6164bc9744 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 @@ -605,19 +605,20 @@ chop_fun (n - 1) ran_T |>> cons dom_T | chop_fun _ _ = raise Fail "unexpected non-function" -fun 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) - end - handle TYPE _ => T_args +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) + end + handle TYPE _ => T_args fun enforce_type_arg_policy_in_combterm ctxt nonmono_Ts type_sys = let