src/Pure/unify.ML
changeset 2193 b7e59795c75b
parent 2178 acb0afbf61a3
child 2753 bcde71e5f371
--- a/src/Pure/unify.ML	Mon Nov 18 16:28:40 1996 +0100
+++ b/src/Pure/unify.ML	Mon Nov 18 16:30:06 1996 +0100
@@ -85,11 +85,11 @@
 		| None   => raise SAME)
 	  | hnorm (Abs(a,T,body)) =  Abs(a, T, hnorm body)
 	  | hnorm (Abs(_,_,body) $ t) =
-	      head_norm (env, subst_bounds([t], body))
+	      head_norm (env, subst_bound (t, body))
 	  | hnorm (f $ t) =
 	      (case hnorm f of
 		 Abs(_,_,body) =>
-		   head_norm (env, subst_bounds([t], body))
+		   head_norm (env, subst_bound (t, body))
 	       | nf => nf $ t)
 	  | hnorm _ =  raise SAME
     in  hnorm t  handle SAME=> t  end