tuned signature -- slightly more general operations (cf. term.ML);

--- a/src/Pure/envir.ML	Fri May 24 14:31:44 2013 +0200
+++ b/src/Pure/envir.ML	Fri May 24 15:13:25 2013 +0200
@@ -33,6 +33,9 @@
   val head_norm: env -> term -> term
   val eta_contract: term -> term
   val beta_eta_contract: term -> term
+  val body_type: env -> int -> typ -> typ
+  val binder_types: env -> int -> typ -> typ list
+  val strip_type: env -> int -> typ -> typ list * typ
   val fastype: env -> typ list -> term -> typ
   val subst_type_same: Type.tyenv -> typ Same.operation
   val subst_term_types_same: Type.tyenv -> term Same.operation
@@ -273,6 +276,24 @@
 end;
 
 
+fun body_type _ 0 T = T
+  | body_type env n (Type ("fun", [_, T])) = body_type env (n - 1) T
+  | body_type env n (T as TVar v) =
+      (case Type.lookup (type_env env) v of
+        NONE => T
+      | SOME T' => body_type env n T')
+  | body_type _ _ T = T;
+
+fun binder_types _ 0 _ = []
+  | binder_types env n (Type ("fun", [T, U])) = T :: binder_types env (n - 1) U
+  | binder_types env n (TVar v) =
+      (case Type.lookup (type_env env) v of
+        NONE => []
+      | SOME T' => binder_types env n T')
+  | binder_types _ _ _ = [];
+
+fun strip_type n env T = (binder_types n env T, body_type n env T);
+
 (*finds type of term without checking that combinations are consistent
   Ts holds types of bound variables*)
 fun fastype (Envir {tyenv, ...}) =
@@ -292,7 +313,6 @@
   in fast end;
 
 
-
 (** plain substitution -- without variable chasing **)
 
 local

--- a/src/Pure/unify.ML	Fri May 24 14:31:44 2013 +0200
+++ b/src/Pure/unify.ML	Fri May 24 15:13:25 2013 +0200
@@ -54,30 +54,6 @@
 
 type dpair = binderlist * term * term;
 
-fun body_type env =
-  let
-    val tyenv = Envir.type_env env;
-    fun bT (Type ("fun", [_, T])) = bT T
-      | bT (T as TVar v) =
-          (case Type.lookup tyenv v of
-            NONE => T
-          | SOME T' => bT T')
-      | bT T = T;
-  in bT end;
-
-fun binder_types env =
-  let
-    val tyenv = Envir.type_env env;
-    fun bTs (Type ("fun", [T, U])) = T :: bTs U
-      | bTs (TVar v) =
-          (case Type.lookup tyenv v of
-            NONE => []
-          | SOME T' => bTs T')
-      | bTs _ = [];
-  in bTs end;
-
-fun strip_type env T = (binder_types env T, body_type env T);
-
 fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t;
 
 
@@ -234,7 +210,7 @@
   let val vT as (v,T) = get_eta_var (rbinder, 0, t) in
     (case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
       NoOcc =>
-        let val env = unify_types thy (body_type env T, fastype env (rbinder, u)) env
+        let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env
         in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end
     | Nonrigid => raise ASSIGN
     | Rigid => raise CANTUNIFY)
@@ -283,7 +259,7 @@
     (case (head_of t, head_of u) of
       (Var (_, T), Var (_, U)) =>
         let
-          val T' = body_type env T and U' = body_type env U;
+          val T' = Envir.body_type env ~1 T and U' = Envir.body_type env ~1 U;
           val env = unify_types thy (T', U') env;
         in (env, dp :: flexflex, flexrigid) end
     | (Var _, _) =>
@@ -340,7 +316,7 @@
   | types_abs (T :: Ts, u) = Abs ("", T, types_abs (Ts, u));
 
 (*Abstraction over the binder of a type*)
-fun type_abs (env, T, t) = types_abs (binder_types env T, t);
+fun type_abs (env, T, t) = types_abs (Envir.binder_types env ~1 T, t);
 
 
 (*MATCH taking "big steps".
@@ -366,7 +342,7 @@
         fun copyargs [] = Seq.cons ([], ed) Seq.empty
           | copyargs (uarg :: uargs) = Seq.maps (copycons uarg) (copyargs uargs);
         val (uhead, uargs) = strip_comb u;
-        val base = body_type env (fastype env (rbinder, uhead));
+        val base = Envir.body_type env ~1 (fastype env (rbinder, uhead));
         fun joinargs (uargs', ed') = (list_comb (uhead, uargs'), ed');
         (*attempt projection on argument with given typ*)
         val Ts = map (curry (fastype env) rbinder) targs;
@@ -395,7 +371,7 @@
           | make_projs _ = raise TERM ("make_projs", u::targs);
         (*try projections and imitation*)
         fun matchfun ((bvar,T,targ)::projs) =
-             (projenv(bvar, strip_type env T, targ, matchfun projs))
+             (projenv(bvar, Envir.strip_type env ~1 T, targ, matchfun projs))
           | matchfun [] = (*imitation last of all*)
             (case uhead of
          Const _ => Seq.map joinargs (copyargs uargs)
@@ -422,7 +398,7 @@
 fun MATCH thy (env, (rbinder, t, u), dpairs) : (Envir.env * dpair list) Seq.seq =
   let
     val (Var (vT as (v, T)), targs) = strip_comb t;
-    val Ts = binder_types env T;
+    val Ts = Envir.binder_types env ~1 T;
     fun new_dset (u', (env', dpairs')) =
       (*if v was updated to s, must unify s with u' *)
       (case Envir.lookup env' vT of
@@ -442,7 +418,7 @@
   let val vT as (v, T) = get_eta_var (rbinder, 0, t) in
     if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
     else
-      let val env = unify_types thy (body_type env T, fastype env (rbinder, u)) env
+      let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env
       in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end
   end;
 
@@ -522,7 +498,7 @@
 fun clean_term banned (env,t) =
   let
     val (Var (v, T), ts) = strip_comb t;
-    val (Ts, U) = strip_type env T
+    val (Ts, U) = Envir.strip_type env ~1 T
     and js = length ts - 1  downto 0;
     val args = sort_args (fold_rev (change_arg banned) (flexargs (js, ts, Ts)) [])
     val ts' = map #t args;
@@ -664,7 +640,7 @@
   let
     val vT as (v, T) = var_head_of (env, t)
     and wU as (w, U) = var_head_of (env, u);
-    val (env', var) = Envir.genvar (#1 v) (env, body_type env T);
+    val (env', var) = Envir.genvar (#1 v) (env, Envir.body_type env ~1 T);
     val env'' = Envir.vupdate (wU, type_abs (env', U, var)) env';
   in
     if vT = wU then env''  (*the other update would be identical*)