make "filter_type_args" more robust if the actual arity is higher than the declared one
authorblanchet
Wed Sep 07 09:10:41 2011 +0200 (2011-09-07)
changeset 447703b1b4d805441
parent 44769 15102294a166
child 44771 0e5d4388bbac
make "filter_type_args" more robust if the actual arity is higher than the declared one
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 09:10:41 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 09:10:41 2011 +0200
     1.3 @@ -1379,7 +1379,7 @@
     1.4  fun chop_fun 0 T = ([], T)
     1.5    | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
     1.6      chop_fun (n - 1) ran_T |>> cons dom_T
     1.7 -  | chop_fun _ _ = raise Fail "unexpected non-function"
     1.8 +  | chop_fun _ T = ([], T)
     1.9  
    1.10  fun filter_type_args _ _ _ [] = []
    1.11    | filter_type_args thy s arity T_args =