# HG changeset patch
# User haftmann
# Date 1277890731 -7200
# Node ID fc27be4c6b1cbecf4c7f022e376e71ad268835e2
# Parent  5b6733e6e033e38115ac402fd401b14b049aa443
unfold_fun_n

diff -r 5b6733e6e033 -r fc27be4c6b1c src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Jun 30 11:38:51 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Jun 30 11:38:51 2010 +0200
@@ -40,6 +40,7 @@
   val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
   val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
   val unfold_fun: itype -> itype list * itype
+  val unfold_fun_n: int -> itype -> itype list * itype
   val unfold_app: iterm -> iterm * iterm list
   val unfold_abs: iterm -> (vname option * itype) list * iterm
   val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
@@ -396,6 +397,13 @@
   (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
     | _ => NONE);
 
+fun unfold_fun_n n ty =
+  let
+    val (tys1, ty1) = unfold_fun ty;
+    val (tys3, tys2) = chop n tys1;
+    val ty3 = Library.foldr (fn (ty1, ty2) => fun_tyco `%% [ty1, ty2]) (tys2, ty1);
+  in (tys3, ty3) end;
+
 end; (* local *)