make "filter_type_args" more robust if the actual arity is higher than the declared one
authorblanchet
Wed, 07 Sep 2011 09:10:41 +0200
changeset 44770 3b1b4d805441
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
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 09:10:41 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 09:10:41 2011 +0200
@@ -1379,7 +1379,7 @@
 fun chop_fun 0 T = ([], T)
   | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
     chop_fun (n - 1) ran_T |>> cons dom_T
-  | chop_fun _ _ = raise Fail "unexpected non-function"
+  | chop_fun _ T = ([], T)
 
 fun filter_type_args _ _ _ [] = []
   | filter_type_args thy s arity T_args =