equal
deleted
inserted
replaced
1377 in aux end |
1377 in aux end |
1378 |
1378 |
1379 fun chop_fun 0 T = ([], T) |
1379 fun chop_fun 0 T = ([], T) |
1380 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) = |
1380 | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) = |
1381 chop_fun (n - 1) ran_T |>> cons dom_T |
1381 chop_fun (n - 1) ran_T |>> cons dom_T |
1382 | chop_fun _ _ = raise Fail "unexpected non-function" |
1382 | chop_fun _ T = ([], T) |
1383 |
1383 |
1384 fun filter_type_args _ _ _ [] = [] |
1384 fun filter_type_args _ _ _ [] = [] |
1385 | filter_type_args thy s arity T_args = |
1385 | filter_type_args thy s arity T_args = |
1386 let |
1386 let |
1387 val U = robust_const_type thy s |
1387 val U = robust_const_type thy s |