| author | haftmann |
| Mon, 20 Dec 2010 08:55:36 +0100 | |
| changeset 41299 | fc8419fd4735 |
| parent 41298 | aad679ca38d2 (diff) |
| parent 41297 | 01b2de947cff (current diff) |
| child 41304 | c7699379a72f |
| child 41313 | a96ac4d180b7 |
| src/HOL/HOLCF/Bifinite.thy | file | annotate | diff | comparison | revisions | |
| src/HOL/HOLCF/CompactBasis.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Tools/type_lifting.ML Sun Dec 19 18:38:50 2010 -0800 +++ b/src/HOL/Tools/type_lifting.ML Mon Dec 20 08:55:36 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);