Type.lookup now curried

--- a/src/HOL/Tools/refute.ML	Wed Mar 19 07:20:31 2008 +0100
+++ b/src/HOL/Tools/refute.ML	Wed Mar 19 07:20:32 2008 +0100
@@ -451,7 +451,7 @@
   fun monomorphic_term typeSubs t =
     map_types (map_type_tvar
       (fn v =>
-        case Type.lookup (typeSubs, v) of
+        case Type.lookup typeSubs v of
           NONE =>
           (* schematic type variable not instantiated *)
           raise REFUTE ("monomorphic_term",

--- a/src/Pure/Proof/reconstruct.ML	Wed Mar 19 07:20:31 2008 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Wed Mar 19 07:20:32 2008 +0100
@@ -68,7 +68,7 @@
     Sign.string_of_typ thy T ^ "\n\n" ^ Sign.string_of_typ thy U);
 
 fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) =
-      (case Type.lookup (iTs, ixnS) of NONE => T | SOME T' => chaseT env T')
+      (case Type.lookup iTs ixnS of NONE => T | SOME T' => chaseT env T')
   | chaseT _ T = T;
 
 fun infer_type thy (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs

--- a/src/Pure/envir.ML	Wed Mar 19 07:20:31 2008 +0100
+++ b/src/Pure/envir.ML	Wed Mar 19 07:20:32 2008 +0100
@@ -151,7 +151,7 @@
 
 fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
   | normT iTs (TFree _) = raise SAME
-  | normT iTs (TVar vS) = (case Type.lookup (iTs, vS) of
+  | normT iTs (TVar vS) = (case Type.lookup iTs vS of
           SOME U => normTh iTs U
         | NONE => raise SAME)
 and normTh iTs T = ((normT iTs T) handle SAME => T)
@@ -256,7 +256,7 @@
         (case fast Ts f of
            Type ("fun", [_, T]) => T
          | TVar ixnS =>
-                (case Type.lookup (iTs, ixnS) of
+                (case Type.lookup iTs ixnS of
                    SOME (Type ("fun", [_, T])) => T
                  | _ => raise TERM (funerr, [f $ u]))
          | _ => raise TERM (funerr, [f $ u]))
@@ -275,7 +275,7 @@
   let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
         | subst(T as TFree _) = T
         | subst(T as TVar ixnS) =
-            (case Type.lookup (iTs, ixnS) of NONE => T | SOME(U) => U)
+            (case Type.lookup iTs ixnS of NONE => T | SOME(U) => U)
   in subst T end;
 
 (*Substitute for type Vars in a term*)

--- a/src/Pure/proofterm.ML	Wed Mar 19 07:20:31 2008 +0100
+++ b/src/Pure/proofterm.ML	Wed Mar 19 07:20:32 2008 +0100
@@ -421,12 +421,12 @@
 
 fun del_conflicting_tvars envT T = TermSubst.instantiateT
   (map_filter (fn ixnS as (_, S) =>
-     (Type.lookup (envT, ixnS); NONE) handle TYPE _ =>
+     (Type.lookup envT ixnS; NONE) handle TYPE _ =>
         SOME (ixnS, TFree ("'dummy", S))) (typ_tvars T)) T;
 
 fun del_conflicting_vars env t = TermSubst.instantiate
   (map_filter (fn ixnS as (_, S) =>
-     (Type.lookup (type_env env, ixnS); NONE) handle TYPE _ =>
+     (Type.lookup (type_env env) ixnS; NONE) handle TYPE _ =>
         SOME (ixnS, TFree ("'dummy", S))) (term_tvars t),
    map_filter (fn Var (ixnT as (_, T)) =>
      (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>

--- a/src/Pure/unify.ML	Wed Mar 19 07:20:31 2008 +0100
+++ b/src/Pure/unify.ML	Wed Mar 19 07:20:32 2008 +0100
@@ -55,14 +55,14 @@
 
 fun body_type(Envir.Envir{iTs,...}) =
 let fun bT(Type("fun",[_,T])) = bT T
-      | bT(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of
+      | bT(T as TVar ixnS) = (case Type.lookup iTs ixnS of
     NONE => T | SOME(T') => bT T')
       | bT T = T
 in bT end;
 
 fun binder_types(Envir.Envir{iTs,...}) =
 let fun bTs(Type("fun",[T,U])) = T :: bTs U
-      | bTs(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of
+      | bTs(T as TVar ixnS) = (case Type.lookup iTs ixnS of
     NONE => [] | SOME(T') => bTs T')
       | bTs _ = []
 in bTs end;
@@ -77,7 +77,7 @@
   let fun etif (Type("fun",[T,U]), t) =
       Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
   | etif (TVar ixnS, t) =
-      (case Type.lookup (iTs, ixnS) of
+      (case Type.lookup iTs ixnS of
       NONE => t | SOME(T) => etif(T,t))
   | etif (_,t) = t;
       fun eta_nm (rbinder, Abs(a,T,body)) =