diff -r c4264f71dc3b -r 4ffe819a9b11 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Wed May 29 11:53:31 2013 +0200
+++ b/src/Pure/envir.ML	Wed May 29 12:03:58 2013 +0200
@@ -35,9 +35,9 @@
   val eta_contract: term -> term
   val beta_eta_contract: term -> term
   val aeconv: term * term -> bool
-  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 body_type: env -> typ -> typ
+  val binder_types: env -> typ -> typ list
+  val strip_type: env -> 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
@@ -298,23 +298,21 @@
 fun aeconv (t, u) = t aconv u orelse eta_contract t aconv eta_contract u;
 
 
-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) =
+fun body_type env (Type ("fun", [_, T])) = body_type env T
+  | body_type env (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;
+      | SOME T' => body_type env 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) =
+fun binder_types env (Type ("fun", [T, U])) = T :: binder_types env U
+  | binder_types env (TVar v) =
       (case Type.lookup (type_env env) v of
         NONE => []
-      | SOME T' => binder_types env n T')
-  | binder_types _ _ _ = [];
+      | SOME T' => binder_types env T')
+  | binder_types _ _ = [];
 
-fun strip_type n env T = (binder_types n env T, body_type n env T);
+fun strip_type env T = (binder_types env T, body_type env T);
 
 (*finds type of term without checking that combinations are consistent
   Ts holds types of bound variables*)