tuned argument_type_of;
authorwenzelm
Thu May 10 00:39:54 2007 +0200 (2007-05-10)
changeset 22908ed66fbbe4a62
parent 22907 dccd0763ae37
child 22909 7de3b0ac4189
tuned argument_type_of;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Thu May 10 00:39:53 2007 +0200
     1.2 +++ b/src/Pure/term.ML	Thu May 10 00:39:54 2007 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4    val aT: sort -> typ
     1.5    val itselfT: typ -> typ
     1.6    val a_itselfT: typ
     1.7 -  val argument_type_of: term -> typ
     1.8 +  val argument_type_of: term -> int -> typ
     1.9    val head_name_of: term -> string
    1.10    val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
    1.11    val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
    1.12 @@ -357,7 +357,7 @@
    1.13  fun fastype_of t : typ = fastype_of1 ([],t);
    1.14  
    1.15  (*Determine the argument type of a function*)
    1.16 -fun argument_type_of tm =
    1.17 +fun argument_type_of tm k =
    1.18    let
    1.19      fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U
    1.20        | argT _ T = raise TYPE ("argument_type_of", [T], []);
    1.21 @@ -366,7 +366,7 @@
    1.22        | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t
    1.23        | arg i Ts (t $ _) = arg (i + 1) Ts t
    1.24        | arg i Ts a = argT i (fastype_of1 (Ts, a));
    1.25 -  in arg 0 [] tm end;
    1.26 +  in arg k [] tm end;
    1.27  
    1.28  
    1.29  val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));