# HG changeset patch
# User haftmann
# Date 1292831736 -3600
# Node ID fc8419fd47353c56e8c28d440f5d6ae133d9353f
# Parent  aad679ca38d2ac0b1b6020c31ef66fb3659ba85b# Parent  01b2de947cff28b62c4ea60c3bab6d0b11408590
merge

diff -r 01b2de947cff -r fc8419fd4735 src/HOL/HOLCF/Bifinite.thy
diff -r 01b2de947cff -r fc8419fd4735 src/HOL/Tools/type_lifting.ML
--- 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);