src/Pure/unify.ML
changeset 2193 b7e59795c75b
parent 2178 acb0afbf61a3
child 2753 bcde71e5f371
     1.1 --- a/src/Pure/unify.ML	Mon Nov 18 16:28:40 1996 +0100
     1.2 +++ b/src/Pure/unify.ML	Mon Nov 18 16:30:06 1996 +0100
     1.3 @@ -85,11 +85,11 @@
     1.4  		| None   => raise SAME)
     1.5  	  | hnorm (Abs(a,T,body)) =  Abs(a, T, hnorm body)
     1.6  	  | hnorm (Abs(_,_,body) $ t) =
     1.7 -	      head_norm (env, subst_bounds([t], body))
     1.8 +	      head_norm (env, subst_bound (t, body))
     1.9  	  | hnorm (f $ t) =
    1.10  	      (case hnorm f of
    1.11  		 Abs(_,_,body) =>
    1.12 -		   head_norm (env, subst_bounds([t], body))
    1.13 +		   head_norm (env, subst_bound (t, body))
    1.14  	       | nf => nf $ t)
    1.15  	  | hnorm _ =  raise SAME
    1.16      in  hnorm t  handle SAME=> t  end