author | boehmes |
Mon, 20 Dec 2010 09:45:26 +0100 | |
changeset 41304 | c7699379a72f |
parent 41303 | 939f647f0c9e (current diff) |
parent 41299 | fc8419fd4735 (diff) |
child 41305 | 42967939ea81 |
child 41311 | de0c906dfe60 |
child 41320 | 4953e21ac76c |
--- a/src/HOL/Tools/type_lifting.ML Mon Dec 20 09:31:47 2010 +0100 +++ b/src/HOL/Tools/type_lifting.ML Mon Dec 20 09:45:26 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);