src/Pure/unify.ML
changeset 8406 a217b0cd304d
parent 4438 ecfeff48bf0c
child 12231 4a25f04bea61
     1.1 --- a/src/Pure/unify.ML	Fri Mar 10 01:16:19 2000 +0100
     1.2 +++ b/src/Pure/unify.ML	Fri Mar 10 14:57:06 2000 +0100
     1.3 @@ -49,14 +49,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(ixn,_)) = (case assoc(iTs,ixn) of
     1.8 +      | bT(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) 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(ixn,_)) = (case assoc(iTs,ixn) of
    1.16 +      | bTs(T as TVar(ixn,_)) = (case Vartab.lookup (iTs,ixn) of
    1.17  		None => [] | Some(T') => bTs T')
    1.18        | bTs _ = []
    1.19  in bTs end;
    1.20 @@ -104,7 +104,7 @@
    1.21  	(case (fast (rbinder, f)) of
    1.22  	   Type("fun",[_,T]) => T
    1.23  	 | TVar(ixn,_) =>
    1.24 -		(case assoc(iTs,ixn) of
    1.25 +		(case Vartab.lookup (iTs,ixn) of
    1.26  		   Some(Type("fun",[_,T])) => T
    1.27  		 | _ => raise TERM(funerr, [f$u]))
    1.28  	 | _ => raise TERM(funerr, [f$u]))
    1.29 @@ -123,7 +123,7 @@
    1.30    let fun etif (Type("fun",[T,U]), t) =
    1.31  	    Abs("", T, etif(U, incr_boundvars 1 t $ Bound 0))
    1.32  	| etif (TVar(ixn,_),t) = 
    1.33 -	    (case assoc(iTs,ixn) of
    1.34 +	    (case Vartab.lookup (iTs,ixn) of
    1.35  		  None => t | Some(T) => etif(T,t))
    1.36  	| etif (_,t) = t;
    1.37        fun eta_nm (rbinder, Abs(a,T,body)) =