# HG changeset patch # User boehmes # Date 1292834726 -3600 # Node ID c7699379a72f1cfc188b86db5f4a2955871631e0 # Parent 939f647f0c9eae3b5797e14a69e79d2669808e63# Parent fc8419fd47353c56e8c28d440f5d6ae133d9353f merged diff -r 939f647f0c9e -r c7699379a72f src/HOL/HOLCF/Bifinite.thy diff -r 939f647f0c9e -r c7699379a72f src/HOL/Tools/type_lifting.ML --- 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);