tuned argument_type_of;

--- a/src/Pure/term.ML	Thu May 10 00:39:53 2007 +0200
+++ b/src/Pure/term.ML	Thu May 10 00:39:54 2007 +0200
@@ -151,7 +151,7 @@
   val aT: sort -> typ
   val itselfT: typ -> typ
   val a_itselfT: typ
-  val argument_type_of: term -> typ
+  val argument_type_of: term -> int -> typ
   val head_name_of: term -> string
   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
@@ -357,7 +357,7 @@
 fun fastype_of t : typ = fastype_of1 ([],t);
 
 (*Determine the argument type of a function*)
-fun argument_type_of tm =
+fun argument_type_of tm k =
   let
     fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U
       | argT _ T = raise TYPE ("argument_type_of", [T], []);
@@ -366,7 +366,7 @@
       | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t
       | arg i Ts (t $ _) = arg (i + 1) Ts t
       | arg i Ts a = argT i (fastype_of1 (Ts, a));
-  in arg 0 [] tm end;
+  in arg k [] tm end;
 
 
 val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));