src/Pure/unify.ML
changeset 26328 b2d6f520172c
parent 24178 4ff1dc2aa18d
child 26939 1035c89b4c02
     1.1 --- a/src/Pure/unify.ML	Wed Mar 19 07:20:31 2008 +0100
     1.2 +++ b/src/Pure/unify.ML	Wed Mar 19 07:20:32 2008 +0100
     1.3 @@ -55,14 +55,14 @@
     1.4  
     1.5  fun body_type(Envir.Envir{iTs,...}) =
     1.6  let fun bT(Type("fun",[_,T])) = bT T
     1.7 -      | bT(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of
     1.8 +      | bT(T as TVar ixnS) = (case Type.lookup iTs ixnS of
     1.9      NONE => T | SOME(T') => bT T')
    1.10        | bT T = T
    1.11  in bT end;
    1.12  
    1.13  fun binder_types(Envir.Envir{iTs,...}) =
    1.14  let fun bTs(Type("fun",[T,U])) = T :: bTs U
    1.15 -      | bTs(T as TVar ixnS) = (case Type.lookup (iTs, ixnS) of
    1.16 +      | bTs(T as TVar ixnS) = (case Type.lookup iTs ixnS of
    1.17      NONE => [] | SOME(T') => bTs T')
    1.18        | bTs _ = []
    1.19  in bTs end;
    1.20 @@ -77,7 +77,7 @@
    1.21    let fun etif (Type("fun",[T,U]), t) =
    1.22        Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
    1.23    | etif (TVar ixnS, t) =
    1.24 -      (case Type.lookup (iTs, ixnS) of
    1.25 +      (case Type.lookup iTs ixnS of
    1.26        NONE => t | SOME(T) => etif(T,t))
    1.27    | etif (_,t) = t;
    1.28        fun eta_nm (rbinder, Abs(a,T,body)) =