# HG changeset patch # User haftmann # Date 1205907632 -3600 # Node ID b2d6f520172c5524ea91cb20aacf300b7e3a6ac6 # Parent fc8df36e2644e0aa3bc902b8ccdceb7b10853f4d Type.lookup now curried diff -r fc8df36e2644 -r b2d6f520172c src/HOL/Tools/refute.ML --- 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", diff -r fc8df36e2644 -r b2d6f520172c src/Pure/Proof/reconstruct.ML --- 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 diff -r fc8df36e2644 -r b2d6f520172c src/Pure/envir.ML --- 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*) diff -r fc8df36e2644 -r b2d6f520172c src/Pure/proofterm.ML --- 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 _ => diff -r fc8df36e2644 -r b2d6f520172c src/Pure/unify.ML --- 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)) =