| changeset 46219 | 426ed18eba43 |
| parent 42279 | 6da43a5018e2 |
| child 48262 | a0d8abca8d7a |
--- a/src/Pure/unify.ML Sat Jan 14 20:05:58 2012 +0100 +++ b/src/Pure/unify.ML Sat Jan 14 21:16:15 2012 +0100 @@ -339,7 +339,7 @@ in (env', map (fn var => Logic.combound (var, 0, length binder)) vars) end; -(*Abstraction over a list of types, like list_abs*) +(*Abstraction over a list of types*) fun types_abs ([], u) = u | types_abs (T :: Ts, u) = Abs ("", T, types_abs (Ts, u));