Type.lookup now curried
authorhaftmann
Wed Mar 19 07:20:32 2008 +0100 (2008-03-19)
changeset 26328b2d6f520172c
parent 26327 fc8df36e2644
child 26329 3e58e4c67a2a
Type.lookup now curried
src/HOL/Tools/refute.ML
src/Pure/Proof/reconstruct.ML
src/Pure/envir.ML
src/Pure/proofterm.ML
src/Pure/unify.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Wed Mar 19 07:20:31 2008 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed Mar 19 07:20:32 2008 +0100
     1.3 @@ -451,7 +451,7 @@
     1.4    fun monomorphic_term typeSubs t =
     1.5      map_types (map_type_tvar
     1.6        (fn v =>
     1.7 -        case Type.lookup (typeSubs, v) of
     1.8 +        case Type.lookup typeSubs v of
     1.9            NONE =>
    1.10            (* schematic type variable not instantiated *)
    1.11            raise REFUTE ("monomorphic_term",
     2.1 --- a/src/Pure/Proof/reconstruct.ML	Wed Mar 19 07:20:31 2008 +0100
     2.2 +++ b/src/Pure/Proof/reconstruct.ML	Wed Mar 19 07:20:32 2008 +0100
     2.3 @@ -68,7 +68,7 @@
     2.4      Sign.string_of_typ thy T ^ "\n\n" ^ Sign.string_of_typ thy U);
     2.5  
     2.6  fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) =
     2.7 -      (case Type.lookup (iTs, ixnS) of NONE => T | SOME T' => chaseT env T')
     2.8 +      (case Type.lookup iTs ixnS of NONE => T | SOME T' => chaseT env T')
     2.9    | chaseT _ T = T;
    2.10  
    2.11  fun infer_type thy (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs
     3.1 --- a/src/Pure/envir.ML	Wed Mar 19 07:20:31 2008 +0100
     3.2 +++ b/src/Pure/envir.ML	Wed Mar 19 07:20:32 2008 +0100
     3.3 @@ -151,7 +151,7 @@
     3.4  
     3.5  fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts)
     3.6    | normT iTs (TFree _) = raise SAME
     3.7 -  | normT iTs (TVar vS) = (case Type.lookup (iTs, vS) of
     3.8 +  | normT iTs (TVar vS) = (case Type.lookup iTs vS of
     3.9            SOME U => normTh iTs U
    3.10          | NONE => raise SAME)
    3.11  and normTh iTs T = ((normT iTs T) handle SAME => T)
    3.12 @@ -256,7 +256,7 @@
    3.13          (case fast Ts f of
    3.14             Type ("fun", [_, T]) => T
    3.15           | TVar ixnS =>
    3.16 -                (case Type.lookup (iTs, ixnS) of
    3.17 +                (case Type.lookup iTs ixnS of
    3.18                     SOME (Type ("fun", [_, T])) => T
    3.19                   | _ => raise TERM (funerr, [f $ u]))
    3.20           | _ => raise TERM (funerr, [f $ u]))
    3.21 @@ -275,7 +275,7 @@
    3.22    let fun subst(Type(a, Ts)) = Type(a, map subst Ts)
    3.23          | subst(T as TFree _) = T
    3.24          | subst(T as TVar ixnS) =
    3.25 -            (case Type.lookup (iTs, ixnS) of NONE => T | SOME(U) => U)
    3.26 +            (case Type.lookup iTs ixnS of NONE => T | SOME(U) => U)
    3.27    in subst T end;
    3.28  
    3.29  (*Substitute for type Vars in a term*)
     4.1 --- a/src/Pure/proofterm.ML	Wed Mar 19 07:20:31 2008 +0100
     4.2 +++ b/src/Pure/proofterm.ML	Wed Mar 19 07:20:32 2008 +0100
     4.3 @@ -421,12 +421,12 @@
     4.4  
     4.5  fun del_conflicting_tvars envT T = TermSubst.instantiateT
     4.6    (map_filter (fn ixnS as (_, S) =>
     4.7 -     (Type.lookup (envT, ixnS); NONE) handle TYPE _ =>
     4.8 +     (Type.lookup envT ixnS; NONE) handle TYPE _ =>
     4.9          SOME (ixnS, TFree ("'dummy", S))) (typ_tvars T)) T;
    4.10  
    4.11  fun del_conflicting_vars env t = TermSubst.instantiate
    4.12    (map_filter (fn ixnS as (_, S) =>
    4.13 -     (Type.lookup (type_env env, ixnS); NONE) handle TYPE _ =>
    4.14 +     (Type.lookup (type_env env) ixnS; NONE) handle TYPE _ =>
    4.15          SOME (ixnS, TFree ("'dummy", S))) (term_tvars t),
    4.16     map_filter (fn Var (ixnT as (_, T)) =>
    4.17       (Envir.lookup (env, ixnT); NONE) handle TYPE _ =>
     5.1 --- a/src/Pure/unify.ML	Wed Mar 19 07:20:31 2008 +0100
     5.2 +++ b/src/Pure/unify.ML	Wed Mar 19 07:20:32 2008 +0100
     5.3 @@ -55,14 +55,14 @@
     5.4  
     5.5  fun body_type(Envir.Envir{iTs,...}) =
     5.6  let fun bT(Type("fun",[_,T])) = bT T
     5.7 -      | bT(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of
     5.8 +      | bT(T as TVar ixnS) = (case Type.lookup iTs ixnS of
     5.9      NONE => T | SOME(T') => bT T')
    5.10        | bT T = T
    5.11  in bT end;
    5.12  
    5.13  fun binder_types(Envir.Envir{iTs,...}) =
    5.14  let fun bTs(Type("fun",[T,U])) = T :: bTs U
    5.15 -      | bTs(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of
    5.16 +      | bTs(T as TVar ixnS) = (case Type.lookup iTs ixnS of
    5.17      NONE => [] | SOME(T') => bTs T')
    5.18        | bTs _ = []
    5.19  in bTs end;
    5.20 @@ -77,7 +77,7 @@
    5.21    let fun etif (Type("fun",[T,U]), t) =
    5.22        Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
    5.23    | etif (TVar ixnS, t) =
    5.24 -      (case Type.lookup (iTs, ixnS) of
    5.25 +      (case Type.lookup iTs ixnS of
    5.26        NONE => t | SOME(T) => etif(T,t))
    5.27    | etif (_,t) = t;
    5.28        fun eta_nm (rbinder, Abs(a,T,body)) =