author | haftmann |
Fri, 17 Dec 2010 22:00:54 +0100 | |
changeset 41298 | aad679ca38d2 |
parent 41257 | a47133170dd0 |
child 41299 | fc8419fd4735 |
--- a/src/HOL/Tools/type_lifting.ML Fri Dec 17 21:32:06 2010 +0100 +++ b/src/HOL/Tools/type_lifting.ML Fri Dec 17 22:00:54 2010 +0100 @@ -80,7 +80,7 @@ let val names = Name.invents nctxt n k; in (names, fold Name.declare names nctxt) end; - val (((vs1, vs2), vs3), _) = Name.context + val (((vs3, vs2), vs1), _) = Name.context |> invents Name.aT (length variances) ||>> invents Name.aT (length variances) ||>> invents Name.aT (length variances);